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

Theorem nsyl 113
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 111 . 2  |-  ( ch 
->  -.  ph )
43con2i 112 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con3i  127  intnand  882  intnanrd  883  ax12  1888  ax6  2099  ax12from12o  2108  camestres  2260  camestros  2264  calemes  2271  calemos  2274  pssn2lp  3290  sotrieq  4357  ordnbtwn  4499  dfwe2  4589  funun  5312  canth  6310  pwuninel2  6315  swoer  6704  swoord1  6705  swoord2  6706  php2  7062  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnflem2  7408  en3lp  7434  rankxpsuc  7568  cardmin2  7647  infxpenlem  7657  cardaleph  7732  isfin4-3  7957  fin23lem24  7964  fin23lem25  7966  fin23lem26  7967  fin23lem38  7991  isfin32i  8007  fin34  8032  fin67  8037  nd3  8227  fpwwe2lem13  8280  canthnum  8287  canthwe  8289  pwfseq  8302  gchcdaidm  8306  gchxpidm  8307  winainflem  8331  r1wunlim  8375  suplem2pr  8693  elnnz  10050  fzneuz  10879  fzodisj  10916  hasheq0  11369  cnpart  11741  sqreulem  11859  rlimuni  12040  rlimcld2  12068  divalglem6  12613  bitsfzo  12642  bitsmod  12643  bitsf1  12653  sadadd2lem2  12657  infpnlem1  12973  ramubcl  13081  ressress  13221  mreexmrid  13561  gsum2d  15239  ablfacrplem  15316  mplsubrglem  16199  infil  17574  fbasfip  17579  fgcl  17589  fin1aufil  17643  hauspwpwf1  17698  ovolicc2lem4  18895  ovolioo  18941  i1fima2sn  19051  itg1addlem4  19070  itgsplitioo  19208  lhop1lem  19376  chordthmlem  20145  ressatans  20246  ftalem5  20330  ppiprm  20405  chtprm  20407  lgsdir2lem2  20579  dirith2  20693  ballotlemfp1  23066  erdszelem8  23744  nodenselem7  24412  nobndup  24425  nobnddown  24426  axlowdimlem13  24654  axlowdim1  24659  nandsym1  24933  onsucsuccmpi  24954  onint1  24960  areacirclem5  25032  intn3an1d  25039  intn3an2d  25040  intn3an3d  25041  nn0prpwlem  26341  nn0prpw  26342  ivthALT  26361  prtlem90  26826  irrapx1  27016  hdmaplem1  32583  hdmaplem2N  32584  hdmaplem3  32585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator