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

Theorem sylnib 331
 Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnib.1 (𝜑 → ¬ 𝜓)
sylnib.2 (𝜓𝜒)
Assertion
Ref Expression
sylnib (𝜑 → ¬ 𝜒)

Proof of Theorem sylnib
StepHypRef Expression
1 sylnib.1 . 2 (𝜑 → ¬ 𝜓)
2 sylnib.2 . . 3 (𝜓𝜒)
32biimpri 231 . 2 (𝜒𝜓)
41, 3nsyl 142 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  sylnibr  332  neqcomd  2811  ssnelpss  4042  fr3nr  7478  omopthi  8271  inf3lem6  9084  rankxpsuc  9299  cflim2  9678  ssfin4  9725  fin23lem30  9757  isf32lem5  9772  gchhar  10094  qextlt  12588  qextle  12589  fzneuz  12987  vdwnn  16327  psgnunilem3  18619  efgredlemb  18867  gsumzsplit  19043  lspexchn2  19899  lspindp2l  19902  lspindp2  19903  psrlidm  20644  mplcoe1  20708  mplcoe5  20711  ptopn2  22192  regr1lem2  22348  rnelfmlem  22560  hauspwpwf1  22595  tsmssplit  22760  reconn  23436  itg2splitlem  24355  itg2split  24356  itg2cn  24370  wilthlem2  25657  bposlem9  25879  2sqcoprm  26022  elntg2  26782  nfrgr2v  28060  hatomistici  30148  nn0min  30565  fedgmullem2  31114  qqhf  31335  hasheuni  31452  oddpwdc  31720  ballotlemimin  31871  ballotlemfrcn0  31895  bnj1388  32413  prv1n  32786  efrunt  33047  dfon2lem4  33139  dfon2lem7  33142  nandsym1  33878  atbase  36578  llnbase  36798  lplnbase  36823  lvolbase  36867  dalem48  37009  lhpbase  37287  cdlemg17pq  37961  cdlemg19  37973  cdlemg21  37975  dvh3dim3N  38738  rmspecnonsq  39835  setindtr  39952  flcidc  40105  scotteld  40941  fmul01lt1lem2  42214  icccncfext  42516  stoweidlem14  42643  stoweidlem26  42655  stirlinglem5  42707  fourierdlem42  42778  fourierdlem62  42797  fourierdlem66  42801  hoicvr  43174
 Copyright terms: Public domain W3C validator