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

Theorem sylnbi 322
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 312 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 209 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198
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 199
This theorem is referenced by:  sylnbir  323  reuun2  4136  opswap  5876  iotanul  6114  riotaund  6919  ndmovcom  7098  suppssov1  7609  suppssfv  7613  brtpos  7643  snnen2o  8437  ranklim  9004  rankuni  9023  cdacomen  9338  ituniiun  9579  hashprb  13499  1mavmul  20759  nonbooli  29082  disjunsn  29970  bj-rest10b  33615  ndmaovcl  42244  ndmaovcom  42246  lindslinindsimp1  43261
  Copyright terms: Public domain W3C validator