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	|- ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))

Proof of Theorem bi2.04

Step	Hyp	Ref	Expression
1		pm2.04 76	. 2 |- ((ph -> (ps -> ch)) -> (ps -> (ph -> ch)))
2		pm2.04 76	. 2 |- ((ps -> (ph -> ch)) -> (ph -> (ps -> ch)))
3	1, 2	impbii 180	1 |- ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))

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