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

Theorem sylnbi 331
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 321 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 218 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  sylnbir  332  reuun2  4283  opswap  6079  iotanul  6326  riotaund  7142  ndmovcom  7324  suppssov1  7851  suppssfv  7855  brtpos  7890  snnen2o  8695  ranklim  9261  rankuni  9280  ituniiun  9832  hashprb  13746  1mavmul  21085  nonbooli  29355  disjunsn  30272  bj-rest10b  34274  disjrnmpt2  41325  ndmaovcl  43279  ndmaovcom  43281  lindslinindsimp1  44440
  Copyright terms: Public domain W3C validator