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

Theorem sylnbi 320
 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 310 . 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  321  reuun2  3902  opswap  5610  iotanul  5854  riotaund  6632  ndmovcom  6806  suppssov1  7312  suppssfv  7316  brtpos  7346  snnen2o  8134  ranklim  8692  rankuni  8711  cdacomen  8988  ituniiun  9229  hashprb  13168  1mavmul  20335  nonbooli  28480  disjunsn  29379  bj-rest10b  33017  ndmaovcl  41046  ndmaovcom  41048  lindslinindsimp1  42011
 Copyright terms: Public domain W3C validator