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  844  imimorb  953  sbrimvw  2097  sbrim  2311  ralcom3  3088  r19.21t  3232  elabgtOLDOLD  3617  reu8  3680  sbccomlem  3808  unissb  4884  reusv3  5343  fun11  6567  xpord3inddlem  8098  oeordi  8517  marypha1lem  9340  aceq1  10033  pwfseqlem3  10577  prime  12604  raluz2  12841  rlimresb  15521  isprm3  16646  isprm4  16647  acsfn  17619  pgpfac1  20051  pgpfac  20055  isdomn5  20681  fbfinnfr  23819  wilthlem3  27050  onsfi  28365  isch3  31330  elat2  32429  mh-unprimbi  36745  fvineqsneq  37745  isat3  39770  cdleme32fva  40900  indstrd  42649  elmapintrab  44024  ntrneik2  44540  ntrneix2  44541  ntrneikb  44542  pm10.541  44815  pm10.542  44816