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  907  intnanrd  908  intn3an1d  1329  intn3an2d  1330  intn3an3d  1331  ax10  2206  ax13fromc9  2215  camestres  2400  camestros  2404  calemes  2411  calemos  2414  pssn2lp  3571  sotrieq  4785  ordnbtwn  4926  funun  5579  canth  6180  dfwe2  6526  pwuninel2  6927  swoer  7263  swoord1  7264  swoord2  7265  php2  7630  en3lp  7959  cantnfp1lem1  8023  cantnfp1lem3  8025  cantnflem2  8035  cantnfp1lem1OLD  8049  cantnfp1lem3OLD  8051  rankxpsuc  8226  cardmin2  8305  infxpenlem  8317  cardaleph  8396  isfin4-3  8621  fin23lem24  8628  fin23lem25  8630  fin23lem26  8631  fin23lem38  8655  isfin32i  8671  fin34  8696  fin67  8701  nd3  8890  fpwwe2lem13  8946  canthnum  8953  canthwe  8955  pwfseq  8968  gchcdaidm  8972  gchxpidm  8973  winainflem  8997  r1wunlim  9041  suplem2pr  9359  elnnz  10794  fzneuz  11686  fzodisj  11728  hasheq0  12288  swrd0  12485  cnpart  12887  sqreulem  13005  rlimuni  13186  rlimcld2  13214  divalglem6  13760  bitsf1  13800  infpnlem1  14129  ramubcl  14237  ressress  14394  mreexmrid  14740  gsum2d  16632  gsum2dOLD  16633  dprddomprc  16657  ablfacrplem  16741  mplsubrglem  17694  mplsubrglemOLD  17695  mdetunilem6  18691  mdetunilem9  18694  madugsum  18717  infil  19835  fbasfip  19840  fgcl  19850  fin1aufil  19904  hauspwpwf1  19959  ovolicc2lem4  21402  ovolioo  21449  i1fima2sn  21558  itg1addlem4  21577  itgsplitioo  21715  lhop1lem  21885  chordthmlem  22627  ressatans  22729  ftalem5  22814  ppiprm  22889  chtprm  22891  lgsdir2lem2  23063  dirith2  23177  axlowdimlem13  23669  axlowdim1  23674  eulerpartlemgvv  27215  ballotlemfp1  27330  ballotlem4  27337  ballotlemirc  27370  erdszelem8  27542  nodenselem7  28284  nobndup  28297  nobnddown  28298  nandsym1  28724  onsucsuccmpi  28745  onint1  28751  fin2solem  28875  mblfinlem1  28888  mblfinlem2  28889  dvasin  28940  dvacos  28941  areacirclem4  28947  nn0prpwlem  28977  nn0prpw  28978  ivthALT  28990  prtlem90  29462  irrapx1  29629  cncfiooicclem1  30461  stoweidlem35  30564  stirlinglem5  30607  frgra2v  31468  rng1nfld  31799  lmod1zrnlvec  31808  sineq0ALT  32516  hdmaplem1  36267  hdmaplem2N  36268  hdmaplem3  36269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator