Theorem bi2.04 387

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	⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

Proof of Theorem bi2.04

Step	Hyp	Ref	Expression
1		pm2.04 90	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2		pm2.04 90	. 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	impbii 209	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imim21b  394  pm4.87  843  imimorb  952  sbrimvw  2096  sbrim  2308  ralcom3  3084  r19.21t  3228  elabgtOLDOLD  3626  reu8  3689  sbccomlem  3817  unissb  4894  reusv3  5348  fun11  6564  xpord3inddlem  8094  oeordi  8513  marypha1lem  9334  aceq1  10025  pwfseqlem3  10569  prime  12571  raluz2  12808  rlimresb  15486  isprm3  16608  isprm4  16609  acsfn  17580  pgpfac1  20009  pgpfac  20013  isdomn5  20641  fbfinnfr  23783  wilthlem3  27034  onsfi  28316  isch3  31265  elat2  32364  fvineqsneq  37556  isat3  39506  cdleme32fva  40636  indstrd  42386  elmapintrab  43759  ntrneik2  44275  ntrneix2  44276  ntrneikb  44277  pm10.541  44550  pm10.542  44551