MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnbi 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
sylnbi.2
Assertion
Ref Expression
sylnbi

Proof of Theorem sylnbi
StepHypRef Expression
1 sylnbi.1 . . 3
21notbii 296 . 2
3 sylnbi.2 . 2
42, 3sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  sylnbir  307  reuun2  3780  opswap  5500  iotanul  5571  riotaund  6293  ndmovcom  6462  suppssov1  6951  suppssfv  6955  brtpos  6983  snnen2o  7726  ranklim  8283  rankuni  8302  cdacomen  8582  ituniiun  8823  hashprb  12462  1mavmul  19050  frgrancvvdeqlem2  25031  frgrawopreglem3  25046  nonbooli  26569  disjunsn  27453  ndmaovcl  32288  ndmaovcom  32290  lindslinindsimp1  33058
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
  Copyright terms: Public domain W3C validator