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

Theorem sylnbi 333
 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 323 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 220 1 𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  sylnbir  334  reuun2  4241  opswap  6057  iotanul  6306  riotaund  7136  ndmovcom  7319  suppssov1  7849  suppssfv  7853  brtpos  7888  snnen2o  8695  ranklim  9261  rankuni  9280  ituniiun  9837  hashprb  13758  1mavmul  21157  nonbooli  29438  disjunsn  30361  bj-rest10b  34505  disjrnmpt2  41808  ndmaovcl  43752  ndmaovcom  43754  lindslinindsimp1  44859  setrec2lem1  45216
 Copyright terms: Public domain W3C validator