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  5358  iotanul  5435  ndmovcom  6236  brtpos  6490  riotav  6556  riotaprc  6589  ranklim  7772  rankuni  7791  cdacomen  8063  ituniiun  8304  hashprb  11670  nonbooli  23155  ndmaovcl  28045  ndmaovcom  28047  frgrancvvdeqlem2  28482  frgrawopreglem3  28497
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 179
  Copyright terms: Public domain W3C validator