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  396  pm4.87  842  imimorb  950  sbrimvw  2095  sbrim  2301  ralcom3  3098  r19.21vOLD  3181  r19.21t  3251  elabgt  3663  reu8  3730  unissb  4944  unissbOLD  4945  reusv3  5404  fun11  6623  xpord3inddlem  8140  oeordi  8587  marypha1lem  9428  aceq1  10112  pwfseqlem3  10655  prime  12643  raluz2  12881  rlimresb  15509  isprm3  16620  isprm4  16621  acsfn  17603  pgpfac1  19950  pgpfac  19954  isdomn5  20917  fbfinnfr  23345  wilthlem3  26574  isch3  30494  elat2  31593  fvineqsneq  36293  isat3  38177  cdleme32fva  39308  elmapintrab  42327  ntrneik2  42843  ntrneix2  42844  ntrneikb  42845  pm10.541  43126  pm10.542  43127