Theorem bi2.04 389

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imim21b  395  pm4.87  840  imimorb  948  sbrimvw  2094  sbrim  2301  r19.21vOLD  3114  r19.21t  3139  elabgt  3603  reu8  3668  unissb  4873  reusv3  5328  fun11  6508  oeordi  8418  marypha1lem  9192  aceq1  9873  pwfseqlem3  10416  prime  12401  raluz2  12637  rlimresb  15274  isprm3  16388  isprm4  16389  acsfn  17368  pgpfac1  19683  pgpfac  19687  fbfinnfr  22992  wilthlem3  26219  isch3  29603  elat2  30702  fvineqsneq  35583  isat3  37321  cdleme32fva  38451  isdomn5  40171  elmapintrab  41184  ntrneik2  41702  ntrneix2  41703  ntrneikb  41704  pm10.541  41985  pm10.542  41986