Theorem bi2.04 375

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  imim21b  381  pm4.87  606  imimorb  917  r19.21t  2938  r19.21v  2943  reu8  3369  unissb  4405  reusv3  4802  fun11  5877  oeordi  7554  marypha1lem  8222  aceq1  8823  pwfseqlem3  9361  prime  11334  raluz2  11613  rlimresb  14144  isprm3  15234  isprm4  15235  acsfn  16143  pgpfac1  18302  pgpfac  18306  fbfinnfr  21455  wilthlem3  24596  isch3  27482  elat2  28583  isat3  33612  cdleme32fva  34743  elmapintrab  36901  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  pm10.541  37588  pm10.542  37589