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

Theorem nsyl 116
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 114 . 2
43con2i 115 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  con3i  130  intnand  892  intnanrd  893  intn3an1d  1313  intn3an2d  1314  intn3an3d  1315  ax10  2188  ax13fromc9  2197  camestres  2371  camestros  2375  calemes  2382  calemos  2385  pssn2lp  3434  sotrieq  4639  ordnbtwn  4780  funun  5432  canth  6017  dfwe2  6363  pwuninel2  6752  swoer  7090  swoord1  7091  swoord2  7092  php2  7455  en3lp  7769  cantnfp1lem1  7833  cantnfp1lem3  7835  cantnflem2  7845  cantnfp1lem1OLD  7859  cantnfp1lem3OLD  7861  rankxpsuc  8036  cardmin2  8115  infxpenlem  8127  cardaleph  8206  isfin4-3  8431  fin23lem24  8438  fin23lem25  8440  fin23lem26  8441  fin23lem38  8465  isfin32i  8481  fin34  8506  fin67  8511  nd3  8700  fpwwe2lem13  8755  canthnum  8762  canthwe  8764  pwfseq  8777  gchcdaidm  8781  gchxpidm  8782  winainflem  8806  r1wunlim  8850  suplem2pr  9168  elnnz  10601  fzneuz  11482  fzodisj  11524  hasheq0  12072  swrd0  12268  cnpart  12670  sqreulem  12788  rlimuni  12969  rlimcld2  12997  divalglem6  13542  bitsf1  13582  infpnlem1  13911  ramubcl  14019  ressress  14175  mreexmrid  14521  gsum2d  16355  ablfacrplem  16432  mplsubrglem  17325  mdetunilem6  18125  mdetunilem9  18128  madugsum  18153  infil  19140  fbasfip  19145  fgcl  19155  fin1aufil  19209  hauspwpwf1  19264  ovolicc2lem4  20703  ovolioo  20749  i1fima2sn  20858  itg1addlem4  20877  itgsplitioo  21015  lhop1lem  21185  chordthmlem  21968  ressatans  22070  ftalem5  22155  ppiprm  22230  chtprm  22232  lgsdir2lem2  22404  dirith2  22518  axlowdimlem13  22879  axlowdim1  22884  eulerpartlemgvv  26462  ballotlemfp1  26577  ballotlem4  26584  ballotlemirc  26617  erdszelem8  26789  nodenselem7  27530  nobndup  27543  nobnddown  27544  nandsym1  27971  onsucsuccmpi  27992  onint1  27998  fin2solem  28086  mblfinlem1  28099  mblfinlem2  28100  dvasin  28151  dvacos  28152  areacirclem4  28158  nn0prpwlem  28188  nn0prpw  28189  ivthALT  28201  prtlem90  28674  irrapx1  28842  stoweidlem35  29504  stirlinglem5  29547  frgra2v  30265  gsumX2d  30504  rng1nfld  30611  lmod1zrnlvec  30620  sineq0ALT  31251  hdmaplem1  34853  hdmaplem2N  34854  hdmaplem3  34855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator