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

Theorem sylnbi 329
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 319 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 216 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  sylnbir  330  reuun2  4317  opswap  6240  iotanul  6532  riotaund  7420  ndmovcom  7613  suppssov1  8212  suppssov2  8213  suppssfv  8217  brtpos  8250  snnen2oOLD  9261  ranklim  9887  rankuni  9906  ituniiun  10465  hashprb  14414  1mavmul  22541  nonbooli  31584  disjunsn  32514  bj-rest10b  36796  disjrnmpt2  44795  ndmaovcl  46816  ndmaovcom  46818  lindslinindsimp1  47840  setrec2lem1  48439
  Copyright terms: Public domain W3C validator