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

Theorem sylnbi 299
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnbi.1  |-  ( ph  <->  ps )
sylnbi.2  |-  ( -. 
ps  ->  ch )
Assertion
Ref Expression
sylnbi  |-  ( -. 
ph  ->  ch )

Proof of Theorem sylnbi
StepHypRef Expression
1 sylnbi.1 . . 3  |-  ( ph  <->  ps )
21notbii 289 . 2  |-  ( -. 
ph 
<->  -.  ps )
3 sylnbi.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylbi 189 1  |-  ( -. 
ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  sylnbir  300  reuun2  3626  opswap  5359  iotanul  5436  ndmovcom  6237  brtpos  6491  riotav  6557  riotaprc  6590  ranklim  7773  rankuni  7792  cdacomen  8066  ituniiun  8307  hashprb  11673  nonbooli  23158  ndmaovcl  28057  ndmaovcom  28059  frgrancvvdeqlem2  28494  frgrawopreglem3  28509
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 179
  Copyright terms: Public domain W3C validator