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

Theorem sylnbir 334
 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 227 . 2 (𝜑𝜓)
3 sylnbir.2 . 2 𝜓𝜒)
42, 3sylnbi 333 1 𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  naecoms  2443  fvmptex  6763  f0cli  6845  1st2val  7703  2nd2val  7704  mpoxopxprcov0  7870  rankvaln  9216  alephcard  9485  alephnbtwn  9486  cfub  9664  cardcf  9667  cflecard  9668  cfle  9669  cflim2  9678  cfidm  9690  itunitc1  9835  ituniiun  9837  domtriom  9858  alephreg  9997  pwcfsdom  9998  cfpwsdom  9999  adderpq  10371  mulerpq  10372  sumz  15074  sumss  15076  prod1  15293  prodss  15296  sn-00id  39526  grur1cld  40927  afvres  43715  afvco2  43719  ndmaovcl  43746
 Copyright terms: Public domain W3C validator