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 208 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
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  394  pm4.87  842  imimorb  949  sbrimvw  2087  sbrim  2294  ralcom3  3094  r19.21vOLD  3177  r19.21t  3247  elabgtOLD  3661  reu8  3728  unissb  4942  unissbOLD  4943  reusv3  5405  fun11  6627  xpord3inddlem  8159  oeordi  8608  marypha1lem  9457  aceq1  10141  pwfseqlem3  10684  prime  12674  raluz2  12912  rlimresb  15542  isprm3  16654  isprm4  16655  acsfn  17639  pgpfac1  20037  pgpfac  20041  isdomn5  21249  fbfinnfr  23758  wilthlem3  27015  isch3  31064  elat2  32163  fvineqsneq  36891  isat3  38779  cdleme32fva  39910  elmapintrab  43006  ntrneik2  43522  ntrneix2  43523  ntrneikb  43524  pm10.541  43804  pm10.542  43805
  Copyright terms: Public domain W3C validator