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  2088  sbrim  2302  ralcom3  3094  r19.21vOLD  3178  r19.21t  3250  elabgtOLD  3672  reu8  3741  sbccomlem  3877  unissb  4943  unissbOLD  4944  reusv3  5410  fun11  6641  xpord3inddlem  8177  oeordi  8623  marypha1lem  9470  aceq1  10154  pwfseqlem3  10697  prime  12696  raluz2  12936  rlimresb  15597  isprm3  16716  isprm4  16717  acsfn  17703  pgpfac1  20114  pgpfac  20118  isdomn5  20726  fbfinnfr  23864  wilthlem3  27127  isch3  31269  elat2  32368  fvineqsneq  37394  isat3  39288  cdleme32fva  40419  indstrd  42174  elmapintrab  43565  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  pm10.541  44362  pm10.542  44363