MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyl Structured version   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  |-  ( ph  ->  -.  ps )
nsyl.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
nsyl  |-  ( ph  ->  -.  ch )

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3  |-  ( ph  ->  -.  ps )
2 nsyl.2 . . 3  |-  ( ch 
->  ps )
31, 2nsyl3 119 . 2  |-  ( ch 
->  -.  ph )
43con2i 120 1  |-  ( ph  ->  -.  ch )
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  135  intnand  907  intnanrd  908  intn3an1d  1329  intn3an2d  1330  intn3an3d  1331  ax10  2206  ax13fromc9  2215  camestres  2400  camestros  2404  calemes  2411  calemos  2414  pssn2lp  3564  sotrieq  4775  ordnbtwn  4916  funun  5567  canth  6157  dfwe2  6502  pwuninel2  6902  swoer  7238  swoord1  7239  swoord2  7240  php2  7605  en3lp  7932  cantnfp1lem1  7996  cantnfp1lem3  7998  cantnflem2  8008  cantnfp1lem1OLD  8022  cantnfp1lem3OLD  8024  rankxpsuc  8199  cardmin2  8278  infxpenlem  8290  cardaleph  8369  isfin4-3  8594  fin23lem24  8601  fin23lem25  8603  fin23lem26  8604  fin23lem38  8628  isfin32i  8644  fin34  8669  fin67  8674  nd3  8863  fpwwe2lem13  8919  canthnum  8926  canthwe  8928  pwfseq  8941  gchcdaidm  8945  gchxpidm  8946  winainflem  8970  r1wunlim  9014  suplem2pr  9332  elnnz  10766  fzneuz  11657  fzodisj  11699  hasheq0  12247  swrd0  12444  cnpart  12846  sqreulem  12964  rlimuni  13145  rlimcld2  13173  divalglem6  13719  bitsf1  13759  infpnlem1  14088  ramubcl  14196  ressress  14353  mreexmrid  14699  gsum2d  16584  gsum2dOLD  16585  dprddomprc  16603  ablfacrplem  16687  mplsubrglem  17640  mplsubrglemOLD  17641  mdetunilem6  18554  mdetunilem9  18557  madugsum  18580  infil  19567  fbasfip  19572  fgcl  19582  fin1aufil  19636  hauspwpwf1  19691  ovolicc2lem4  21134  ovolioo  21181  i1fima2sn  21290  itg1addlem4  21309  itgsplitioo  21447  lhop1lem  21617  chordthmlem  22359  ressatans  22461  ftalem5  22546  ppiprm  22621  chtprm  22623  lgsdir2lem2  22795  dirith2  22909  axlowdimlem13  23351  axlowdim1  23356  eulerpartlemgvv  26902  ballotlemfp1  27017  ballotlem4  27024  ballotlemirc  27057  erdszelem8  27229  nodenselem7  27971  nobndup  27984  nobnddown  27985  nandsym1  28411  onsucsuccmpi  28432  onint1  28438  fin2solem  28562  mblfinlem1  28575  mblfinlem2  28576  dvasin  28627  dvacos  28628  areacirclem4  28634  nn0prpwlem  28664  nn0prpw  28665  ivthALT  28677  prtlem90  29149  irrapx1  29316  stoweidlem35  29977  stirlinglem5  30020  frgra2v  30738  rng1nfld  31145  lmod1zrnlvec  31154  sineq0ALT  31990  hdmaplem1  35739  hdmaplem2N  35740  hdmaplem3  35741
  Copyright terms: Public domain W3C validator