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:  fvmptex  5781  f0cli  5851  1st2val  6601  2nd2val  6602  mpt2xopxprcov0  6733  rankvaln  8002  alephcard  8236  alephnbtwn  8237  cfub  8414  cardcf  8417  cflecard  8418  cfle  8419  cflim2  8428  cfidm  8440  itunitc1  8585  ituniiun  8587  domtriom  8608  alephreg  8742  pwcfsdom  8743  cfpwsdom  8744  adderpq  9121  mulerpq  9122  sumz  13195  sumss  13197  eleenn  23077  prod1  27386  prodss  27389  afvres  30003  afvco2  30007  ndmaovcl  30034
  Copyright terms: Public domain W3C validator