Theorem bi2.04 376

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 90	. 2 |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) )
2		pm2.04 90	. 2 |- ( ( ps -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) )
3	1, 2	impbii 199	1 |- ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) )

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

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 197

This theorem is referenced by:  imim21b  382  pm4.87  608  imimorb  921  r19.21t  2955  r19.21v  2960  reu8  3402  unissb  4469  reusv3  4876  fun11  5963  oeordi  7667  marypha1lem  8339  aceq1  8940  pwfseqlem3  9482  prime  11458  raluz2  11737  rlimresb  14296  isprm3  15396  isprm4  15397  acsfn  16320  pgpfac1  18479  pgpfac  18483  fbfinnfr  21645  wilthlem3  24796  isch3  28098  elat2  29199  isat3  34594  cdleme32fva  35725  elmapintrab  37882  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  pm10.541  38566  pm10.542  38567