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

Theorem sylnbir 298
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 193 . 2  |-  ( ph  <->  ps )
3 sylnbir.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylnbi 297 1  |-  ( -. 
ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  fvmptex  5626  f0cli  5687  1st2val  6161  2nd2val  6162  rankvaln  7487  alephcard  7713  alephnbtwn  7714  cfub  7891  cardcf  7894  cflecard  7895  cfle  7896  cflim2  7905  cfidm  7917  itunitc1  8062  ituniiun  8064  domtriom  8085  alephreg  8220  pwcfsdom  8221  cfpwsdom  8222  adderpq  8596  mulerpq  8597  sumz  12211  sumss  12213  prod1  24169  eleenn  24596  matrcl  27569  afvres  28140  afvco2  28144  ndmaovcl  28171  mpt2xopxprcov0  28199
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator