Theorem bi2.04 361

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

Assertion

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

Proof of Theorem bi2.04

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

Syntax hints:   -> wi 4   <-> wb 184

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 185

This theorem is referenced by:  imim21b  367  pm4.87  584  imimorb  872  sbcom2OLD  2161  r19.21t  2907  reu8  3262  ra4  3390  unissb  4232  reusv3  4609  fun11  5592  oeordi  7137  marypha1lem  7795  aceq1  8399  pwfseqlem3  8939  prime  10834  raluz2  11016  rlimresb  13162  isprm3  13891  isprm4  13892  acsfn  14717  pgpfac1  16704  pgpfac  16708  fbfinnfr  19547  wilthlem3  22542  isch3  24797  elat2  25897  pm10.541  29768  pm10.542  29769  isat3  33291  cdleme32fva  34420