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

Theorem sylnbir 300
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 195 . 2  |-  ( ph  <->  ps )
3 sylnbir.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylnbi 299 1  |-  ( -. 
ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  fvmptex  5817  f0cli  5882  1st2val  6374  2nd2val  6375  mpt2xopxprcov0  6470  rankvaln  7727  alephcard  7953  alephnbtwn  7954  cfub  8131  cardcf  8134  cflecard  8135  cfle  8136  cflim2  8145  cfidm  8157  itunitc1  8302  ituniiun  8304  domtriom  8325  alephreg  8459  pwcfsdom  8460  cfpwsdom  8461  adderpq  8835  mulerpq  8836  sumz  12518  sumss  12520  prod1  25272  prodss  25275  eleenn  25837  afvres  28014  afvco2  28018  ndmaovcl  28045
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 179
  Copyright terms: Public domain W3C validator