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  2026  fvmptex  5959  f0cli  6031  1st2val  6810  2nd2val  6811  mpt2xopxprcov0  6945  rankvaln  8216  alephcard  8450  alephnbtwn  8451  cfub  8628  cardcf  8631  cflecard  8632  cfle  8633  cflim2  8642  cfidm  8654  itunitc1  8799  ituniiun  8801  domtriom  8822  alephreg  8956  pwcfsdom  8957  cfpwsdom  8958  adderpq  9333  mulerpq  9334  sumz  13506  sumss  13508  eleenn  23891  prod1  28669  prodss  28672  afvres  31740  afvco2  31744  ndmaovcl  31771
  Copyright terms: Public domain W3C validator