Theorem bi2.04 392

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 91	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2		pm2.04 91	. 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	impbii 212	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imim21b  400  pm4.87  857  imimorb  965  sbrimvwOLD  2129  sbrim  2341  ralcom3  3117  r19.21t  3261  reu8  3698  sbccomlem  3824  unissb  4908  reusv3  5378  fun11  6614  xpord3inddlem  8156  oeordi  8579  marypha1lem  9400  aceq1  10117  pwfseqlem3  10662  prime  12695  raluz2  12939  rlimresb  15642  isprm3  16765  isprm4  16766  acsfn  17739  pgpfac1  20198  pgpfac  20202  isdomn5  20861  fbfinnfr  24051  wilthlem3  27287  onsfi  28602  isch3  31666  elat2  32765  mh-unprimbi  37114  fvineqsneq  38117  isat3  40141  cdleme32fva  41271  indstrd  43020  elmapintrab  44362  ntrneik2  44878  ntrneix2  44879  ntrneikb  44880  pm10.541  45137  pm10.542  45138