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  5340  fun11  6564  xpord3inddlem  8095  oeordi  8514  marypha1lem  9337  aceq1  10028  pwfseqlem3  10572  prime  12574  raluz2  12811  rlimresb  15489  isprm3  16611  isprm4  16612  acsfn  17583  pgpfac1  20015  pgpfac  20019  isdomn5  20645  fbfinnfr  23784  wilthlem3  27020  onsfi  28336  isch3  31301  elat2  32400  fvineqsneq  37724  isat3  39744  cdleme32fva  40874  indstrd  42624  elmapintrab  44006  ntrneik2  44522  ntrneix2  44523  ntrneikb  44524  pm10.541  44797  pm10.542  44798