MPE Home 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