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

Theorem sylnbir 305
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 304 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  2059  fvmptex  5868  f0cli  5944  1st2val  6725  2nd2val  6726  mpt2xopxprcov0  6863  rankvaln  8130  alephcard  8364  alephnbtwn  8365  cfub  8542  cardcf  8545  cflecard  8546  cfle  8547  cflim2  8556  cfidm  8568  itunitc1  8713  ituniiun  8715  domtriom  8736  alephreg  8870  pwcfsdom  8871  cfpwsdom  8872  adderpq  9245  mulerpq  9246  sumz  13546  sumss  13548  prod1  13753  prodss  13756  eleenn  24320  afvres  32423  afvco2  32427  ndmaovcl  32454
  Copyright terms: Public domain W3C validator