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  2131  sbrim  2341  ralcom3  3116  r19.21t  3260  reu8  3694  sbccomlem  3821  unissb  4906  reusv3  5374  fun11  6644  xpord3inddlem  8208  oeordi  8634  marypha1lem  9462  aceq1  10235  pwfseqlem3  10784  prime  12820  raluz2  13064  rlimresb  15776  isprm3  16902  isprm4  16903  acsfn  17883  pgpfac1  20347  pgpfac  20351  isdomn5  21013  fbfinnfr  24215  wilthlem3  27454  onsfi  28799  isch3  31900  elat2  32999  mh-unprimbi  37547  fvineqsneq  38603  isat3  40630  cdleme32fva  41760  indstrd  43509  elmapintrab  44838  ntrneik2  45353  ntrneix2  45354  ntrneikb  45355  pm10.541  45612  pm10.542  45613