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  2094  sbrim  2306  ralcom3  3082  r19.21t  3226  elabgtOLDOLD  3624  reu8  3687  sbccomlem  3815  unissb  4889  reusv3  5341  fun11  6555  xpord3inddlem  8084  oeordi  8502  marypha1lem  9317  aceq1  10008  pwfseqlem3  10551  prime  12554  raluz2  12795  rlimresb  15472  isprm3  16594  isprm4  16595  acsfn  17565  pgpfac1  19994  pgpfac  19998  isdomn5  20625  fbfinnfr  23756  wilthlem3  27007  onsfi  28283  isch3  31221  elat2  32320  fvineqsneq  37454  isat3  39354  cdleme32fva  40484  indstrd  42234  elmapintrab  43617  ntrneik2  44133  ntrneix2  44134  ntrneikb  44135  pm10.541  44408  pm10.542  44409