Theorem bi2.04 386

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  393  pm4.87  839  imimorb  947  sbrimvw  2092  sbrim  2298  ralcom3  3095  r19.21vOLD  3178  r19.21t  3248  elabgt  3661  reu8  3728  unissb  4942  unissbOLD  4943  reusv3  5402  fun11  6621  xpord3inddlem  8142  oeordi  8589  marypha1lem  9430  aceq1  10114  pwfseqlem3  10657  prime  12647  raluz2  12885  rlimresb  15513  isprm3  16624  isprm4  16625  acsfn  17607  pgpfac1  19991  pgpfac  19995  isdomn5  21117  fbfinnfr  23565  wilthlem3  26810  isch3  30761  elat2  31860  fvineqsneq  36596  isat3  38480  cdleme32fva  39611  elmapintrab  42629  ntrneik2  43145  ntrneix2  43146  ntrneikb  43147  pm10.541  43428  pm10.542  43429