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

Theorem sylnib 328
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 227 . 2 (𝜒𝜓)
41, 3nsyl 140 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:  sylnibr  329  neqcomd  2734  ssnelpss  4103  fr3nr  7752  omopthi  8656  cofonr  8669  inf3lem6  9624  rankxpsuc  9873  cflim2  10254  ssfin4  10301  fin23lem30  10333  isf32lem5  10348  gchhar  10670  qextlt  13179  qextle  13180  fzneuz  13579  vdwnn  16930  psgnunilem3  19406  efgredlemb  19656  gsumzsplit  19837  lspexchn2  20972  lspindp2l  20975  lspindp2  20976  psrlidm  21833  mplcoe1  21902  mplcoe5  21905  ptopn2  23410  regr1lem2  23566  rnelfmlem  23778  hauspwpwf1  23813  tsmssplit  23978  reconn  24666  itg2splitlem  25600  itg2split  25601  itg2cn  25615  wilthlem2  26917  bposlem9  27141  2sqcoprm  27284  elntg2  28712  nfrgr2v  29994  hatomistici  32084  nn0min  32493  fedgmullem2  33194  qqhf  33455  hasheuni  33572  oddpwdc  33842  ballotlemimin  33993  ballotlemfrcn0  34017  bnj1388  34533  prv1n  34911  efrunt  35177  dfon2lem4  35253  dfon2lem7  35256  nandsym1  35797  atbase  38649  llnbase  38870  lplnbase  38895  lvolbase  38939  dalem48  39081  lhpbase  39359  cdlemg17pq  40033  cdlemg19  40045  cdlemg21  40047  dvh3dim3N  40810  rmspecnonsq  42134  setindtr  42252  flcidc  42405  omssrncard  42780  scotteld  43494  fmul01lt1lem2  44786  icccncfext  45088  stoweidlem14  45215  stoweidlem26  45227  stirlinglem5  45279  fourierdlem42  45350  fourierdlem62  45369  fourierdlem66  45373  hoicvr  45749
  Copyright terms: Public domain W3C validator