Theorem bi2.04 388

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  841  imimorb  949  sbrimvw  2094  sbrim  2300  ralcom3  3096  r19.21vOLD  3173  r19.21t  3234  elabgt  3627  reu8  3694  unissb  4905  unissbOLD  4906  reusv3  5365  fun11  6580  xpord3inddlem  8091  oeordi  8539  marypha1lem  9378  aceq1  10062  pwfseqlem3  10605  prime  12593  raluz2  12831  rlimresb  15459  isprm3  16570  isprm4  16571  acsfn  17553  pgpfac1  19873  pgpfac  19877  fbfinnfr  23229  wilthlem3  26456  isch3  30246  elat2  31345  fvineqsneq  35956  isat3  37842  cdleme32fva  38973  isdomn5  40696  elmapintrab  41970  ntrneik2  42486  ntrneix2  42487  ntrneikb  42488  pm10.541  42769  pm10.542  42770