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

Theorem sylnbi 306
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 296 . 2  |-  ( -. 
ph 
<->  -.  ps )
3 sylnbi.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylbi 195 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:  sylnbir  307  reuun2  3781  opswap  5495  iotanul  5566  riotaund  6282  ndmovcom  6447  suppssov1  6933  suppssfv  6937  brtpos  6965  snnen2o  7707  ranklim  8263  rankuni  8282  cdacomen  8562  ituniiun  8803  hashprb  12431  1mavmul  18857  frgrancvvdeqlem2  24805  frgrawopreglem3  24820  nonbooli  26342  ndmaovcl  31982  ndmaovcom  31984  lindslinindsimp1  32356
  Copyright terms: Public domain W3C validator