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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imim21b  394  pm4.87  842  imimorb  949  sbrimvw  2087  sbrim  2294  ralcom3  3094  r19.21vOLD  3177  r19.21t  3247  elabgtOLD  3661  reu8  3728  unissb  4942  unissbOLD  4943  reusv3  5405  fun11  6627  xpord3inddlem  8159  oeordi  8608  marypha1lem  9457  aceq1  10141  pwfseqlem3  10684  prime  12674  raluz2  12912  rlimresb  15542  isprm3  16654  isprm4  16655  acsfn  17639  pgpfac1  20037  pgpfac  20041  isdomn5  21249  fbfinnfr  23758  wilthlem3  27015  isch3  31064  elat2  32163  fvineqsneq  36891  isat3  38779  cdleme32fva  39910  elmapintrab  43006  ntrneik2  43522  ntrneix2  43523  ntrneikb  43524  pm10.541  43804  pm10.542  43805