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

Theorem nsyl 137
Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Hypotheses
Ref Expression
nsyl.1 (𝜑 → ¬ 𝜓)
nsyl.2 (𝜒𝜓)
Assertion
Ref Expression
nsyl (𝜑 → ¬ 𝜒)

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3 (𝜑 → ¬ 𝜓)
2 nsyl.2 . . 3 (𝜒𝜓)
31, 2nsyl3 135 . 2 (𝜒 → ¬ 𝜑)
43con2i 136 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con3i  151  intnand  478  intnanrd  479  intn3an1d  1596  intn3an2d  1597  intn3an3d  1598  camestresOLD  2750  camestrosOLD  2758  calemesOLD  2769  calemosOLD  2775  pssn2lp  3917  sotrieq  5272  ordnbtwn  6041  funun  6156  canth  6842  dfwe2  7221  opabn1stprc  7470  pwuninel2  7645  swoer  8019  swoord1  8020  swoord2  8021  php2  8394  en3lp  8766  cantnfp1lem1  8832  cantnfp1lem3  8834  cantnflem2  8844  rankxpsuc  9002  cardmin2  9117  infxpenlem  9129  cardaleph  9205  isfin4-3  9432  fin23lem24  9439  fin23lem25  9441  fin23lem26  9442  fin23lem38  9466  isfin32i  9482  fin34  9507  fin67  9512  nd3  9706  fpwwe2lem13  9759  canthnum  9766  canthwe  9768  pwfseq  9781  gchcdaidm  9785  gchxpidm  9786  r1wunlim  9854  suplem2pr  10170  elnnz  11673  fzneuz  12664  fzodisj  12746  fzodisjsn  12750  hasheq0  13392  swrd0  13678  cnpart  14223  sqreulem  14342  rlimuni  14524  rlimcld2  14552  divalglem6  15361  bitsf1  15407  infpnlem1  15851  ramubcl  15959  ressress  16170  mreexmrid  16528  gsum2d  18592  dprddomprc  18621  ablfacrplem  18686  rng1nfld  19507  mplsubrglem  19668  mdetunilem6  20655  mdetunilem9  20658  madugsum  20681  infil  21901  fbasfip  21906  fgcl  21916  fin1aufil  21970  hauspwpwf1  22025  ovolicc2lem4  23524  ovolioo  23572  i1fima2sn  23684  itg1addlem4  23703  itgsplitioo  23841  lhop1lem  24013  chordthmlem  24796  ressatans  24898  ftalem5  25040  ppiprm  25114  chtprm  25116  lgsdir2lem2  25288  dirith2  25454  axlowdimlem13  26071  axlowdim1  26076  nfrgr2v  27470  eulerpartlemgvv  30786  ballotlemfp1  30901  ballotlem4  30908  ballotlemirc  30941  erdszelem8  31525  bccolsum  31969  noresle  32189  noetalem3  32208  nn0prpwlem  32660  nn0prpw  32661  ivthALT  32673  nandsym1  32760  onsucsuccmpi  32781  onint1  32787  topdifinffinlem  33530  relowlssretop  33546  fin2solem  33727  poimirlem2  33743  poimirlem3  33744  poimirlem4  33745  poimirlem6  33747  poimirlem7  33748  poimirlem8  33749  poimirlem9  33750  poimirlem13  33754  poimirlem14  33755  poimirlem15  33756  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem21  33762  poimirlem22  33763  poimirlem23  33764  poimirlem26  33767  poimirlem31  33772  mblfinlem1  33778  mblfinlem2  33779  dvasin  33827  dvacos  33828  areacirclem4  33834  ax10fromc7  34693  hdmaplem1  37570  hdmaplem2N  37571  hdmaplem3  37572  irrapx1  37912  gneispace  38950  sineq0ALT  39685  sumnnodd  40360  fperdvper  40631  stoweidlem35  40749  stirlinglem5  40792  fourierdlem68  40888  fourierswlem  40944  fouriersw  40945  zrninitoringc  42657  lmod1zrnlvec  42869  elsetrecslem  43031
  Copyright terms: Public domain W3C validator