Theorem bi2.04 177

Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.

Assertion

Ref	Expression
bi2.04	|- ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))

Proof of Theorem bi2.04

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

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  or12 278  pm4.14 379  pm4.78 381  pm4.87 383  sbcom 1632  sbcom2 1724  mo 1787  2mo 1851  r19.21t 2177  reu8 2448  ra5 2539  unissb 3208  fun11 4480  oeordi 5262  oaabs 5309  aceq1 5891  prime 7407  raluz2 7612  metcnplem 9164  chcmhi 10746  elat2 11912  isprm3 13776  pm10.541 16314  pm10.542 16315

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

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain