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

Theorem nsyl 121
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 119 . 2
43con2i 120 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  con3i  135  intnand  916  intnanrd  917  intn3an1d  1338  intn3an2d  1339  intn3an3d  1340  ax10  2226  ax13fromc9  2235  camestres  2403  camestros  2407  calemes  2414  calemos  2417  pssn2lp  3604  sotrieq  4832  ordnbtwn  4973  funun  5635  canth  6254  dfwe2  6617  pwuninel2  7022  swoer  7358  swoord1  7359  swoord2  7360  php2  7722  en3lp  8054  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnflem2  8130  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  rankxpsuc  8321  cardmin2  8400  infxpenlem  8412  cardaleph  8491  isfin4-3  8716  fin23lem24  8723  fin23lem25  8725  fin23lem26  8726  fin23lem38  8750  isfin32i  8766  fin34  8791  fin67  8796  nd3  8985  fpwwe2lem13  9041  canthnum  9048  canthwe  9050  pwfseq  9063  gchcdaidm  9067  gchxpidm  9068  r1wunlim  9136  suplem2pr  9452  elnnz  10899  fzneuz  11788  fzodisj  11859  hasheq0  12433  swrd0  12658  cnpart  13073  sqreulem  13192  rlimuni  13373  rlimcld2  13401  divalglem6  14056  bitsf1  14096  infpnlem1  14428  ramubcl  14536  ressress  14694  mreexmrid  15040  gsum2d  16999  gsum2dOLD  17000  dprddomprc  17031  ablfacrplem  17116  rng1nfld  17926  mplsubrglem  18100  mplsubrglemOLD  18101  mdetunilem6  19119  mdetunilem9  19122  madugsum  19145  infil  20364  fbasfip  20369  fgcl  20379  fin1aufil  20433  hauspwpwf1  20488  ovolicc2lem4  21931  ovolioo  21978  i1fima2sn  22087  itg1addlem4  22106  itgsplitioo  22244  lhop1lem  22414  chordthmlem  23163  ressatans  23265  ftalem5  23350  ppiprm  23425  chtprm  23427  lgsdir2lem2  23599  dirith2  23713  axlowdimlem13  24257  axlowdim1  24262  frgra2v  24999  eulerpartlemgvv  28315  ballotlemfp1  28430  ballotlem4  28437  ballotlemirc  28470  erdszelem8  28642  nodenselem7  29447  nobndup  29460  nobnddown  29461  nandsym1  29887  onsucsuccmpi  29908  onint1  29914  fin2solem  30039  mblfinlem1  30051  mblfinlem2  30052  dvasin  30103  dvacos  30104  areacirclem4  30110  nn0prpwlem  30140  nn0prpw  30141  ivthALT  30153  prtlem90  30598  irrapx1  30764  sumnnodd  31636  fperdvper  31715  stoweidlem35  31817  stirlinglem5  31860  fourierdlem68  31957  fourierswlem  32013  fouriersw  32014  zrninitoringc  32879  lmod1zrnlvec  33095  sineq0ALT  33737  hdmaplem1  37498  hdmaplem2N  37499  hdmaplem3  37500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator