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  844  imimorb  953  sbrimvw  2097  sbrim  2311  ralcom3  3087  r19.21t  3231  elabgtOLDOLD  3616  reu8  3679  sbccomlem  3807  unissb  4883  reusv3  5347  fun11  6572  xpord3inddlem  8104  oeordi  8523  marypha1lem  9346  aceq1  10039  pwfseqlem3  10583  prime  12610  raluz2  12847  rlimresb  15527  isprm3  16652  isprm4  16653  acsfn  17625  pgpfac1  20057  pgpfac  20061  isdomn5  20687  fbfinnfr  23806  wilthlem3  27033  onsfi  28348  isch3  31312  elat2  32411  mh-unprimbi  36726  fvineqsneq  37728  isat3  39753  cdleme32fva  40883  indstrd  42632  elmapintrab  44003  ntrneik2  44519  ntrneix2  44520  ntrneikb  44521  pm10.541  44794  pm10.542  44795