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

Theorem sylnbir 320
 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 214 . 2 (𝜑𝜓)
3 sylnbir.2 . 2 𝜓𝜒)
42, 3sylnbi 319 1 𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  naecoms  2346  fvmptex  6333  f0cli  6410  1st2val  7238  2nd2val  7239  mpt2xopxprcov0  7388  rankvaln  8700  alephcard  8931  alephnbtwn  8932  cfub  9109  cardcf  9112  cflecard  9113  cfle  9114  cflim2  9123  cfidm  9135  itunitc1  9280  ituniiun  9282  domtriom  9303  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  adderpq  9816  mulerpq  9817  sumz  14497  sumss  14499  prod1  14718  prodss  14721  eleenn  25821  afvres  41573  afvco2  41577  ndmaovcl  41604
 Copyright terms: Public domain W3C validator