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

Theorem sylnbi 297
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 287 . 2  |-  ( -. 
ph 
<->  -.  ps )
3 sylnbi.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylbi 187 1  |-  ( -. 
ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  sylnbir  298  reuun2  3451  opswap  5159  iotanul  5234  ndmovcom  6007  brtpos  6243  riotav  6309  riotaprc  6342  ranklim  7516  rankuni  7535  cdacomen  7807  ituniiun  8048  nonbooli  22230  nbssntrs  26147  ndmaovcl  28063  ndmaovcom  28065
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