Theorem bi2.04 376

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  imim21b  382  pm4.87  858  imimorb  962  r19.21t  3107  r19.21v  3112  reu8  3560  unissb  4616  reusv3  5019  fun11  6114  oeordi  7842  marypha1lem  8516  aceq1  9161  pwfseqlem3  9705  prime  11682  raluz2  11961  rlimresb  14526  isprm3  15624  isprm4  15625  acsfn  16547  pgpfac1  18707  pgpfac  18711  fbfinnfr  21885  wilthlem3  25038  isch3  28455  elat2  29556  isat3  35131  cdleme32fva  36262  elmapintrab  38422  ntrneik2  38930  ntrneix2  38931  ntrneikb  38932  pm10.541  39106  pm10.542  39107