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  843  imimorb  952  sbrimvw  2091  sbrim  2304  ralcom3  3086  r19.21vOLD  3166  r19.21t  3236  elabgtOLD  3652  reu8  3716  sbccomlem  3844  unissb  4915  unissbOLD  4916  reusv3  5375  fun11  6610  xpord3inddlem  8153  oeordi  8599  marypha1lem  9445  aceq1  10131  pwfseqlem3  10674  prime  12674  raluz2  12913  rlimresb  15581  isprm3  16702  isprm4  16703  acsfn  17671  pgpfac1  20063  pgpfac  20067  isdomn5  20670  fbfinnfr  23779  wilthlem3  27032  onsfi  28299  isch3  31222  elat2  32321  fvineqsneq  37430  isat3  39325  cdleme32fva  40456  indstrd  42206  elmapintrab  43600  ntrneik2  44116  ntrneix2  44117  ntrneikb  44118  pm10.541  44391  pm10.542  44392