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  3630  reu8  3693  sbccomlem  3821  unissb  4898  reusv3  5352  fun11  6574  xpord3inddlem  8106  oeordi  8525  marypha1lem  9348  aceq1  10039  pwfseqlem3  10583  prime  12585  raluz2  12822  rlimresb  15500  isprm3  16622  isprm4  16623  acsfn  17594  pgpfac1  20023  pgpfac  20027  isdomn5  20655  fbfinnfr  23797  wilthlem3  27048  onsfi  28364  isch3  31329  elat2  32428  fvineqsneq  37667  isat3  39683  cdleme32fva  40813  indstrd  42563  elmapintrab  43932  ntrneik2  44448  ntrneix2  44449  ntrneikb  44450  pm10.541  44723  pm10.542  44724