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  2128  sbrim  2337  ralcom3  3112  r19.21t  3256  reu8  3690  sbccomlem  3817  unissb  4900  reusv3  5367  fun11  6619  xpord3inddlem  8178  oeordi  8604  marypha1lem  9432  aceq1  10203  pwfseqlem3  10752  prime  12787  raluz2  13031  rlimresb  15741  isprm3  16867  isprm4  16868  acsfn  17842  pgpfac1  20305  pgpfac  20309  isdomn5  20971  fbfinnfr  24169  wilthlem3  27406  onsfi  28751  isch3  31852  elat2  32951  mh-unprimbi  37456  fvineqsneq  38472  isat3  40501  cdleme32fva  41631  indstrd  43380  elmapintrab  44714  ntrneik2  45229  ntrneix2  45230  ntrneikb  45231  pm10.541  45488  pm10.542  45489