Theorem bi2.04 392

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 91	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2		pm2.04 91	. 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	impbii 212	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imim21b  400  pm4.87  857  imimorb  965  sbrimvwOLD  2129  sbrim  2337  ralcom3  3112  r19.21t  3256  reu8  3691  sbccomlem  3817  unissb  4901  reusv3  5370  fun11  6608  xpord3inddlem  8153  oeordi  8576  marypha1lem  9404  aceq1  10121  pwfseqlem3  10670  prime  12703  raluz2  12947  rlimresb  15653  isprm3  16774  isprm4  16775  acsfn  17748  pgpfac1  20210  pgpfac  20214  isdomn5  20873  fbfinnfr  24068  wilthlem3  27307  onsfi  28622  isch3  31723  elat2  32822  mh-unprimbi  37164  fvineqsneq  38167  isat3  40181  cdleme32fva  41311  indstrd  43060  elmapintrab  44417  ntrneik2  44933  ntrneix2  44934  ntrneikb  44935  pm10.541  45192  pm10.542  45193