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  3223  elabgtOLDOLD  3629  reu8  3693  sbccomlem  3821  unissb  4890  reusv3  5344  fun11  6556  xpord3inddlem  8087  oeordi  8505  marypha1lem  9323  aceq1  10011  pwfseqlem3  10554  prime  12557  raluz2  12798  rlimresb  15472  isprm3  16594  isprm4  16595  acsfn  17565  pgpfac1  19961  pgpfac  19965  isdomn5  20595  fbfinnfr  23726  wilthlem3  26978  onsfi  28252  isch3  31185  elat2  32284  fvineqsneq  37386  isat3  39286  cdleme32fva  40416  indstrd  42166  elmapintrab  43549  ntrneik2  44065  ntrneix2  44066  ntrneikb  44067  pm10.541  44340  pm10.542  44341