Theorem imsubd-P3.28c 271

Description: Implication Substitution (dual) †.

This can also be called "Linking Syllogism" because the result is the statement that adding the missing inner link between the two hypotheses links the entire chain as a consequence.

The mneumonic is as follows...

If ( 1 → 2 ) and ( 3 → 4 ) then ( ( 2 → 3 ) → ( 1 → 4 ) )...

or ( left-middle → right-middle ) → ( left-outer → right-outer ).

One can substitute ( 1 → 1 ) for ( 1 → 2 ), or ( 3 → 3 ) for ( 3 → 4 ) to see how imsubr-P3.28b 269 and imsubl-P3.28a 267 are related as special cases.

Hypotheses

Ref	Expression
imsubd-P3.28c.1	⊢ (𝛾 → (𝜑 → 𝜓))
imsubd-P3.28c.2	⊢ (𝛾 → (𝜒 → 𝜗))

Assertion

Ref	Expression
imsubd-P3.28c	⊢ (𝛾 → ((𝜓 → 𝜒) → (𝜑 → 𝜗)))

Proof of Theorem imsubd-P3.28c

Step	Hyp	Ref	Expression
1		imsubd-P3.28c.1	. . 3 ⊢ (𝛾 → (𝜑 → 𝜓))
2	1	imsubl-P3.28a 267	. 2 ⊢ (𝛾 → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
3		imsubd-P3.28c.2	. . 3 ⊢ (𝛾 → (𝜒 → 𝜗))
4	3	imsubr-P3.28b 269	. 2 ⊢ (𝛾 → ((𝜑 → 𝜒) → (𝜑 → 𝜗)))
5	2, 4	syl-P3.24 259	1 ⊢ (𝛾 → ((𝜓 → 𝜒) → (𝜑 → 𝜗)))

Syntax hints:   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133

This theorem is referenced by:  imsubd-P3.28c.RC  272  subimd-P3.40c  329  nfrimd-P6  815