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

Theorem sylnbir 307
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnbir.1  |-  ( ps  <->  ph )
sylnbir.2  |-  ( -. 
ps  ->  ch )
Assertion
Ref Expression
sylnbir  |-  ( -. 
ph  ->  ch )

Proof of Theorem sylnbir
StepHypRef Expression
1 sylnbir.1 . . 3  |-  ( ps  <->  ph )
21bicomi 202 . 2  |-  ( ph  <->  ps )
3 sylnbir.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylnbi 306 1  |-  ( -. 
ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  naecoms  2039  fvmptex  5951  f0cli  6027  1st2val  6811  2nd2val  6812  mpt2xopxprcov0  6947  rankvaln  8220  alephcard  8454  alephnbtwn  8455  cfub  8632  cardcf  8635  cflecard  8636  cfle  8637  cflim2  8646  cfidm  8658  itunitc1  8803  ituniiun  8805  domtriom  8826  alephreg  8960  pwcfsdom  8961  cfpwsdom  8962  adderpq  9337  mulerpq  9338  sumz  13523  sumss  13525  eleenn  24071  prod1  29051  prodss  29054  afvres  32095  afvco2  32099  ndmaovcl  32126
  Copyright terms: Public domain W3C validator