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

Theorem nsyl 142
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 140 . 2 (𝜒 → ¬ 𝜑)
43con2i 141 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  157  sylnib  329  intnand  489  intnanrd  490  intn3an1d  1472  intn3an2d  1473  intn3an3d  1474  pssn2lp  4082  sotrieq  5501  ordnbtwn  6279  funun  6397  canth  7103  dfwe2  7484  opabn1stprc  7747  pwuninel2  7931  swoer  8309  swoord1  8310  swoord2  8311  php2  8691  phpeqd  8695  en3lp  9066  cantnfp1lem1  9130  cantnfp1lem3  9132  cantnflem2  9142  rankxpsuc  9300  cardmin2  9416  infxpenlem  9428  cardaleph  9504  isfin4p1  9726  fin23lem24  9733  fin23lem25  9735  fin23lem26  9736  fin23lem38  9760  isfin32i  9776  fin34  9801  fin67  9806  nd3  10000  fpwwe2lem13  10053  canthnum  10060  canthwe  10062  pwfseq  10075  gchdjuidm  10079  gchxpidm  10080  r1wunlim  10148  suplem2pr  10464  elnnz  11980  fzneuz  12978  fzodisj  13061  fzodisjsn  13065  hasheq0  13714  swrd0  14010  cnpart  14589  sqreulem  14709  rlimuni  14897  rlimcld2  14925  divalglem6  15739  bitsf1  15785  infpnlem1  16236  ramubcl  16344  ressress  16552  mreexmrid  16904  gsum2d  19012  dprddomprc  19042  ablfacrplem  19107  trivnsimpgd  19139  ablsimpnosubgd  19146  rng1nfld  19970  mplsubrglem  20138  mdetunilem6  21142  mdetunilem9  21145  madugsum  21168  infil  22387  fbasfip  22392  fgcl  22402  fin1aufil  22456  hauspwpwf1  22511  ovolicc2lem4  24036  ovolioo  24084  i1fima2sn  24196  itg1addlem4  24215  itgsplitioo  24353  lhop1lem  24525  chordthmlem  25323  ressatans  25425  ftalem5  25568  ppiprm  25642  chtprm  25644  lgsdir2lem2  25816  dirith2  26018  axlowdimlem13  26654  axlowdim1  26659  nfrgr2v  27965  eulerpartlemgvv  31520  ballotlemfp1  31635  ballotlem4  31642  ballotlemirc  31675  erdszelem8  32329  bccolsum  32855  frrlem11  33017  frrlem12  33018  noresle  33084  noetalem3  33103  nn0prpwlem  33554  nn0prpw  33555  ivthALT  33567  nandsym1  33654  onsucsuccmpi  33675  onint1  33681  bj-fununsn1  34414  bj-fvmptunsn1  34418  topdifinffinlem  34497  relowlssretop  34513  domalom  34554  fin2solem  34745  poimirlem2  34761  poimirlem3  34762  poimirlem4  34763  poimirlem6  34765  poimirlem7  34766  poimirlem8  34767  poimirlem9  34768  poimirlem13  34772  poimirlem14  34773  poimirlem15  34774  poimirlem16  34775  poimirlem17  34776  poimirlem19  34778  poimirlem20  34779  poimirlem21  34780  poimirlem22  34781  poimirlem23  34782  poimirlem26  34785  poimirlem31  34790  mblfinlem1  34796  mblfinlem2  34797  dvasin  34845  dvacos  34846  areacirclem4  34852  ax10fromc7  35898  hdmaplem1  38774  hdmaplem2N  38775  hdmaplem3  38776  negn0nposznnd  39033  irrapx1  39290  gneispace  40349  mnuprdlem2  40474  sineq0ALT  41136  sumnnodd  41776  fperdvper  42068  stoweidlem35  42186  stirlinglem5  42229  fourierdlem68  42325  fourierswlem  42381  fouriersw  42382  requad1  43619  requad2  43620  zrninitoringc  44174  lmod1zrnlvec  44381  elsetrecslem  44633
  Copyright terms: Public domain W3C validator