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

Theorem sylnbi 329
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 319 . 2 𝜑 ↔ ¬ 𝜓)
3 sylnbi.2 . 2 𝜓𝜒)
42, 3sylbi 216 1 𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  sylnbir  330  reuun2  4274  opswap  6181  iotanul  6474  riotaund  7353  ndmovcom  7541  suppssov1  8129  suppssfv  8133  brtpos  8166  snnen2oOLD  9171  ranklim  9780  rankuni  9799  ituniiun  10358  hashprb  14297  1mavmul  21897  nonbooli  30593  disjunsn  31512  bj-rest10b  35560  disjrnmpt2  43397  ndmaovcl  45425  ndmaovcom  45427  lindslinindsimp1  46528  setrec2lem1  47128
  Copyright terms: Public domain W3C validator