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:  naecoms  2000  fvmptex  5784  f0cli  5854  1st2val  6602  2nd2val  6603  mpt2xopxprcov0  6734  rankvaln  8006  alephcard  8240  alephnbtwn  8241  cfub  8418  cardcf  8421  cflecard  8422  cfle  8423  cflim2  8432  cfidm  8444  itunitc1  8589  ituniiun  8591  domtriom  8612  alephreg  8746  pwcfsdom  8747  cfpwsdom  8748  adderpq  9125  mulerpq  9126  sumz  13199  sumss  13201  eleenn  23142  prod1  27457  prodss  27460  afvres  30078  afvco2  30082  ndmaovcl  30109
  Copyright terms: Public domain W3C validator