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

Theorem sylnbi 308
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 298 . 2  |-  ( -. 
ph 
<->  -.  ps )
3 sylnbi.2 . 2  |-  ( -. 
ps  ->  ch )
42, 3sylbi 199 1  |-  ( -. 
ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  sylnbir  309  reuun2  3757  opswap  5340  iotanul  5578  riotaund  6300  ndmovcom  6468  suppssov1  6956  suppssfv  6960  brtpos  6988  snnen2o  7765  ranklim  8318  rankuni  8337  cdacomen  8613  ituniiun  8854  hashprb  12575  1mavmul  19565  frgrancvvdeqlem2  25751  frgrawopreglem3  25766  nonbooli  27296  disjunsn  28200  ndmaovcl  38423  ndmaovcom  38425  lindslinindsimp1  39556
  Copyright terms: Public domain W3C validator