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  2428  fvmptex  6963  f0cli  7049  1st2val  7950  2nd2val  7951  mpoxopxprcov0  8149  rankvaln  9736  alephcard  10007  alephnbtwn  10008  cfub  10186  cardcf  10189  cflecard  10190  cfle  10191  cflim2  10200  cfidm  10212  itunitc1  10357  ituniiun  10359  domtriom  10380  alephreg  10519  pwcfsdom  10520  cfpwsdom  10521  adderpq  10893  mulerpq  10894  sumz  15608  sumss  15610  prod1  15828  prodss  15831  newval  27188  leftval  27196  rightval  27197  madess  27209  oldssmade  27210  lrold  27229  fpwfvss  41691  grur1cld  42519  afvres  45411  afvco2  45415  ndmaovcl  45442
  Copyright terms: Public domain W3C validator