Theorem bi2.04 350

Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
bi2.04	⊢ ((φ → (ψ → χ)) ↔ (ψ → (φ → χ)))

Proof of Theorem bi2.04

Step	Hyp	Ref	Expression
1		pm2.04 76	. 2 ⊢ ((φ → (ψ → χ)) → (ψ → (φ → χ)))
2		pm2.04 76	. 2 ⊢ ((ψ → (φ → χ)) → (φ → (ψ → χ)))
3	1, 2	impbii 180	1 ⊢ ((φ → (ψ → χ)) ↔ (ψ → (φ → χ)))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  imim21b  356  pm4.87  567  imimorb  847  ax12bOLD  1690  sbcom  2089  sbcom2  2114  r19.21t  2700  reu8  3033  ra5  3131  unissb  3922  fun11  5160  spacind  6288