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

Theorem sylnbir 319
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 212 . 2 (𝜑𝜓)
3 sylnbir.2 . 2 𝜓𝜒)
42, 3sylnbi 318 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  naecoms  2300  fvmptex  6188  f0cli  6263  1st2val  7062  2nd2val  7063  mpt2xopxprcov0  7207  rankvaln  8522  alephcard  8753  alephnbtwn  8754  cfub  8931  cardcf  8934  cflecard  8935  cfle  8936  cflim2  8945  cfidm  8957  itunitc1  9102  ituniiun  9104  domtriom  9125  alephreg  9260  pwcfsdom  9261  cfpwsdom  9262  adderpq  9634  mulerpq  9635  sumz  14246  sumss  14248  prod1  14459  prodss  14462  eleenn  25494  afvres  39706  afvco2  39710  ndmaovcl  39737
  Copyright terms: Public domain W3C validator