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.21vOLD  3159  r19.21t  3231  elabgtOLDOLD  3640  reu8  3704  sbccomlem  3832  unissb  4903  unissbOLD  4904  reusv3  5360  fun11  6590  xpord3inddlem  8133  oeordi  8551  marypha1lem  9384  aceq1  10070  pwfseqlem3  10613  prime  12615  raluz2  12856  rlimresb  15531  isprm3  16653  isprm4  16654  acsfn  17620  pgpfac1  20012  pgpfac  20016  isdomn5  20619  fbfinnfr  23728  wilthlem3  26980  onsfi  28247  isch3  31170  elat2  32269  fvineqsneq  37400  isat3  39300  cdleme32fva  40431  indstrd  42181  elmapintrab  43565  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  pm10.541  44356  pm10.542  44357