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  2096  sbrim  2310  ralcom3  3086  r19.21t  3230  elabgtOLDOLD  3628  reu8  3691  sbccomlem  3819  unissb  4896  reusv3  5350  fun11  6566  xpord3inddlem  8096  oeordi  8515  marypha1lem  9336  aceq1  10027  pwfseqlem3  10571  prime  12573  raluz2  12810  rlimresb  15488  isprm3  16610  isprm4  16611  acsfn  17582  pgpfac1  20011  pgpfac  20015  isdomn5  20643  fbfinnfr  23785  wilthlem3  27036  onsfi  28352  isch3  31316  elat2  32415  fvineqsneq  37617  isat3  39567  cdleme32fva  40697  indstrd  42447  elmapintrab  43817  ntrneik2  44333  ntrneix2  44334  ntrneikb  44335  pm10.541  44608  pm10.542  44609