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

Theorem sylnbi 318
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 308 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 205 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  sylnbir  319  reuun2  3865  opswap  5523  iotanul  5766  riotaund  6521  ndmovcom  6693  suppssov1  7188  suppssfv  7192  brtpos  7222  snnen2o  8008  ranklim  8564  rankuni  8583  cdacomen  8860  ituniiun  9101  hashprb  12995  1mavmul  20112  frgrancvvdeqlem2  26321  frgrawopreglem3  26336  nonbooli  27697  disjunsn  28592  bj-rest10b  32023  ndmaovcl  39734  ndmaovcom  39736  frgrncvvdeqlem2  41469  frgrwopreglem3  41482  lindslinindsimp1  42039
  Copyright terms: Public domain W3C validator