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  2338  ralcom3  3113  r19.21t  3257  reu8  3691  sbccomlem  3817  unissb  4901  reusv3  5367  fun11  6614  xpord3inddlem  8171  oeordi  8596  marypha1lem  9425  aceq1  10196  pwfseqlem3  10745  prime  12780  raluz2  13024  rlimresb  15732  isprm3  16858  isprm4  16859  acsfn  17833  pgpfac1  20296  pgpfac  20300  isdomn5  20962  fbfinnfr  24160  wilthlem3  27397  onsfi  28742  isch3  31843  elat2  32942  mh-unprimbi  37332  fvineqsneq  38335  isat3  40364  cdleme32fva  41494  indstrd  43243  elmapintrab  44576  ntrneik2  45091  ntrneix2  45092  ntrneikb  45093  pm10.541  45350  pm10.542  45351