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  17600  pgpfac1  19996  pgpfac  20000  isdomn5  20630  fbfinnfr  23761  wilthlem3  27013  onsfi  28287  isch3  31220  elat2  32319  fvineqsneq  37393  isat3  39293  cdleme32fva  40424  indstrd  42174  elmapintrab  43558  ntrneik2  44074  ntrneix2  44075  ntrneikb  44076  pm10.541  44349  pm10.542  44350