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

Theorem sylnbi 304
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 294 . 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  305  reuun2  3778  opswap  5478  iotanul  5549  riotaund  6267  ndmovcom  6435  suppssov1  6924  suppssfv  6928  brtpos  6956  snnen2o  7699  ranklim  8253  rankuni  8272  cdacomen  8552  ituniiun  8793  hashprb  12446  1mavmul  19217  frgrancvvdeqlem2  25233  frgrawopreglem3  25248  nonbooli  26767  disjunsn  27664  ndmaovcl  32527  ndmaovcom  32529  lindslinindsimp1  33312
  Copyright terms: Public domain W3C validator