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

Theorem sylnbi 319
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 309 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 207 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  sylnbir  320  reuun2  3943  opswap  5660  iotanul  5904  riotaund  6687  ndmovcom  6863  suppssov1  7372  suppssfv  7376  brtpos  7406  snnen2o  8190  ranklim  8745  rankuni  8764  cdacomen  9041  ituniiun  9282  hashprb  13223  1mavmul  20402  nonbooli  28638  disjunsn  29533  bj-rest10b  33167  ndmaovcl  41604  ndmaovcom  41606  lindslinindsimp1  42571
  Copyright terms: Public domain W3C validator