Theorem bi2.04 388

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 210	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  imim21b  395  pm4.87  849  imimorb  958  sbrimvw  2102  sbrim  2315  ralcom3  3089  r19.21t  3233  reu8  3674  sbccomlem  3801  unissb  4871  reusv3  5334  fun11  6559  xpord3inddlem  8094  oeordi  8513  marypha1lem  9336  aceq1  10030  pwfseqlem3  10574  prime  12601  raluz2  12838  rlimresb  15518  isprm3  16643  isprm4  16644  acsfn  17616  pgpfac1  20048  pgpfac  20052  isdomn5  20682  fbfinnfr  23824  wilthlem3  27051  onsfi  28366  isch3  31330  elat2  32429  mh-unprimbi  36772  fvineqsneq  37774  isat3  39799  cdleme32fva  40929  indstrd  42678  elmapintrab  44020  ntrneik2  44536  ntrneix2  44537  ntrneikb  44538  pm10.541  44811  pm10.542  44812