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  2092  sbrim  2304  ralcom3  3079  r19.21t  3229  elabgtOLDOLD  3637  reu8  3701  sbccomlem  3829  unissb  4899  unissbOLD  4900  reusv3  5355  fun11  6574  xpord3inddlem  8110  oeordi  8528  marypha1lem  9360  aceq1  10046  pwfseqlem3  10589  prime  12591  raluz2  12832  rlimresb  15507  isprm3  16629  isprm4  16630  acsfn  17596  pgpfac1  19988  pgpfac  19992  isdomn5  20595  fbfinnfr  23704  wilthlem3  26956  onsfi  28223  isch3  31143  elat2  32242  fvineqsneq  37373  isat3  39273  cdleme32fva  40404  indstrd  42154  elmapintrab  43538  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  pm10.541  44329  pm10.542  44330