MPE Home 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