MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2.04 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm2.04 90 . 2 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
2 pm2.04 90 . 2 ((𝜓 → (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
31, 2impbii 209 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
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  844  imimorb  953  sbrimvw  2091  sbrim  2304  ralcom3  3097  r19.21vOLD  3181  r19.21t  3253  elabgtOLD  3673  reu8  3739  sbccomlem  3869  unissb  4939  unissbOLD  4940  reusv3  5405  fun11  6640  xpord3inddlem  8179  oeordi  8625  marypha1lem  9473  aceq1  10157  pwfseqlem3  10700  prime  12699  raluz2  12939  rlimresb  15601  isprm3  16720  isprm4  16721  acsfn  17702  pgpfac1  20100  pgpfac  20104  isdomn5  20710  fbfinnfr  23849  wilthlem3  27113  isch3  31260  elat2  32359  fvineqsneq  37413  isat3  39308  cdleme32fva  40439  indstrd  42194  elmapintrab  43589  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  pm10.541  44386  pm10.542  44387
  Copyright terms: Public domain W3C validator