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

Theorem sylnbir 331
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnbir.1 (𝜓𝜑)
sylnbir.2 𝜓𝜒)
Assertion
Ref Expression
sylnbir 𝜑𝜒)

Proof of Theorem sylnbir
StepHypRef Expression
1 sylnbir.1 . . 3 (𝜓𝜑)
21bicomi 223 . 2 (𝜑𝜓)
3 sylnbir.2 . 2 𝜓𝜒)
42, 3sylnbi 330 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  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:  naecoms  2429  fvmptex  7010  f0cli  7097  1st2val  8000  2nd2val  8001  mpoxopxprcov0  8199  rankvaln  9791  alephcard  10062  alephnbtwn  10063  cfub  10241  cardcf  10244  cflecard  10245  cfle  10246  cflim2  10255  cfidm  10267  itunitc1  10412  ituniiun  10414  domtriom  10435  alephreg  10574  pwcfsdom  10575  cfpwsdom  10576  adderpq  10948  mulerpq  10949  sumz  15665  sumss  15667  prod1  15885  prodss  15888  newval  27340  leftval  27348  rightval  27349  lltropt  27357  madess  27361  oldssmade  27362  lrold  27381  fpwfvss  42149  grur1cld  42977  afvres  45867  afvco2  45871  ndmaovcl  45898
  Copyright terms: Public domain W3C validator