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  2091  sbrim  2304  ralcom3  3097  r19.21vOLD  3181  r19.21t  3253  elabgtOLD  3673  reu8  3739  sbccomlem  3869  unissb  4939  unissbOLD  4940  reusv3  5405  fun11  6640  xpord3inddlem  8179  oeordi  8625  marypha1lem  9473  aceq1  10157  pwfseqlem3  10700  prime  12699  raluz2  12939  rlimresb  15601  isprm3  16720  isprm4  16721  acsfn  17702  pgpfac1  20100  pgpfac  20104  isdomn5  20710  fbfinnfr  23849  wilthlem3  27113  isch3  31260  elat2  32359  fvineqsneq  37413  isat3  39308  cdleme32fva  40439  indstrd  42194  elmapintrab  43589  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  pm10.541  44386  pm10.542  44387