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  5610  f0cli  5671  1st2val  6145  2nd2val  6146  rankvaln  7471  alephcard  7697  alephnbtwn  7698  cfub  7875  cardcf  7878  cflecard  7879  cfle  7880  cflim2  7889  cfidm  7901  itunitc1  8046  ituniiun  8048  domtriom  8069  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  adderpq  8580  mulerpq  8581  sumz  12195  sumss  12197  eleenn  24524  matrcl  27466  afvres  28034  afvco2  28037  ndmaovcl  28063  mpt2xopxprcov0  28083
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