Theorem pm5.74 235

Description: Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 11-Apr-2013.)

Assertion

Ref	Expression
pm5.74	⊢ ((φ → (ψ ↔ χ)) ↔ ((φ → ψ) ↔ (φ → χ)))

Proof of Theorem pm5.74

Step	Hyp	Ref	Expression
1		bi1 178	. . . 4 ⊢ ((ψ ↔ χ) → (ψ → χ))
2	1	imim3i 55	. . 3 ⊢ ((φ → (ψ ↔ χ)) → ((φ → ψ) → (φ → χ)))
3		bi2 189	. . . 4 ⊢ ((ψ ↔ χ) → (χ → ψ))
4	3	imim3i 55	. . 3 ⊢ ((φ → (ψ ↔ χ)) → ((φ → χ) → (φ → ψ)))
5	2, 4	impbid 183	. 2 ⊢ ((φ → (ψ ↔ χ)) → ((φ → ψ) ↔ (φ → χ)))
6		bi1 178	. . . 4 ⊢ (((φ → ψ) ↔ (φ → χ)) → ((φ → ψ) → (φ → χ)))
7	6	pm2.86d 93	. . 3 ⊢ (((φ → ψ) ↔ (φ → χ)) → (φ → (ψ → χ)))
8		bi2 189	. . . 4 ⊢ (((φ → ψ) ↔ (φ → χ)) → ((φ → χ) → (φ → ψ)))
9	8	pm2.86d 93	. . 3 ⊢ (((φ → ψ) ↔ (φ → χ)) → (φ → (χ → ψ)))
10	7, 9	impbidd 181	. 2 ⊢ (((φ → ψ) ↔ (φ → χ)) → (φ → (ψ ↔ χ)))
11	5, 10	impbii 180	1 ⊢ ((φ → (ψ ↔ χ)) ↔ ((φ → ψ) ↔ (φ → χ)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177

This theorem is used by:  pm5.74i  236  pm5.74ri  237  pm5.74d  238  pm5.74rd  239  bibi2d  309  pm5.32  617  orbidi  898