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  842  imimorb  951  sbrimvw  2091  sbrim  2308  ralcom3  3103  r19.21vOLD  3187  r19.21t  3259  elabgtOLD  3686  reu8  3755  sbccomlem  3891  unissb  4963  unissbOLD  4964  reusv3  5423  fun11  6652  xpord3inddlem  8195  oeordi  8643  marypha1lem  9502  aceq1  10186  pwfseqlem3  10729  prime  12724  raluz2  12962  rlimresb  15611  isprm3  16730  isprm4  16731  acsfn  17717  pgpfac1  20124  pgpfac  20128  isdomn5  20732  fbfinnfr  23870  wilthlem3  27131  isch3  31273  elat2  32372  fvineqsneq  37378  isat3  39263  cdleme32fva  40394  indstrd  42150  elmapintrab  43538  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  pm10.541  44336  pm10.542  44337