Theorem bi2.04 379

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  imim21b  385  pm4.87  876  imimorb  980  r19.21t  3164  r19.21v  3169  reu8  3627  unissb  4691  reusv3  5105  fun11  6196  oeordi  7934  marypha1lem  8608  aceq1  9253  pwfseqlem3  9797  prime  11786  raluz2  12019  rlimresb  14673  isprm3  15768  isprm4  15769  acsfn  16672  pgpfac1  18833  pgpfac  18837  fbfinnfr  22015  wilthlem3  25209  isch3  28653  elat2  29754  isat3  35382  cdleme32fva  36512  elmapintrab  38723  ntrneik2  39230  ntrneix2  39231  ntrneikb  39232  pm10.541  39406  pm10.542  39407