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  3744  opswap  5437  iotanul  5507  riotaund  6200  ndmovcom  6363  suppssov1  6834  suppssfv  6838  brtpos  6867  snnen2o  7613  ranklim  8165  rankuni  8184  cdacomen  8464  ituniiun  8705  hashprb  12278  1mavmul  18489  nonbooli  25226  ndmaovcl  30277  ndmaovcom  30279  frgrancvvdeqlem2  30792  frgrawopreglem3  30807  lindslinindsimp1  31143
  Copyright terms: Public domain W3C validator