Theorem bi2.04 387

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imim21b  394  pm4.87  843  imimorb  952  sbrimvw  2092  sbrim  2304  ralcom3  3080  r19.21vOLD  3160  r19.21t  3232  elabgtOLDOLD  3643  reu8  3707  sbccomlem  3835  unissb  4906  unissbOLD  4907  reusv3  5363  fun11  6593  xpord3inddlem  8136  oeordi  8554  marypha1lem  9391  aceq1  10077  pwfseqlem3  10620  prime  12622  raluz2  12863  rlimresb  15538  isprm3  16660  isprm4  16661  acsfn  17627  pgpfac1  20019  pgpfac  20023  isdomn5  20626  fbfinnfr  23735  wilthlem3  26987  onsfi  28254  isch3  31177  elat2  32276  fvineqsneq  37407  isat3  39307  cdleme32fva  40438  indstrd  42188  elmapintrab  43572  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  pm10.541  44363  pm10.542  44364