Theorem bi2.04 391

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imim21b  399  pm4.87  856  imimorb  965  sbrimvwOLD  2132  sbrim  2345  ralcom3  3121  r19.21t  3265  reu8  3705  sbccomlem  3831  unissb  4910  reusv3  5377  fun11  6611  xpord3inddlem  8149  oeordi  8572  marypha1lem  9392  aceq1  10100  pwfseqlem3  10644  prime  12676  raluz2  12920  rlimresb  15615  isprm3  16740  isprm4  16741  acsfn  17714  pgpfac1  20151  pgpfac  20155  isdomn5  20794  fbfinnfr  23966  wilthlem3  27199  onsfi  28514  isch3  31533  elat2  32632  mh-unprimbi  36943  fvineqsneq  37945  isat3  39970  cdleme32fva  41100  indstrd  42849  elmapintrab  44193  ntrneik2  44709  ntrneix2  44710  ntrneikb  44711  pm10.541  44968  pm10.542  44969