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  ax6  2086  ax12  2095  camestres  2247  camestros  2251  calemes  2258  calemos  2261  pssn2lp  3277  sotrieq  4341  ordnbtwn  4483  dfwe2  4573  funun  5296  canth  6294  pwuninel2  6299  swoer  6688  swoord1  6689  swoord2  6690  php2  7046  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem2  7392  en3lp  7418  rankxpsuc  7552  cardmin2  7631  infxpenlem  7641  cardaleph  7716  isfin4-3  7941  fin23lem24  7948  fin23lem25  7950  fin23lem26  7951  fin23lem38  7975  isfin32i  7991  fin34  8016  fin67  8021  nd3  8211  fpwwe2lem13  8264  canthnum  8271  canthwe  8273  pwfseq  8286  gchcdaidm  8290  gchxpidm  8291  winainflem  8315  r1wunlim  8359  suplem2pr  8677  elnnz  10034  fzneuz  10863  fzodisj  10900  hasheq0  11353  cnpart  11725  sqreulem  11843  rlimuni  12024  rlimcld2  12052  divalglem6  12597  bitsfzo  12626  bitsmod  12627  bitsf1  12637  sadadd2lem2  12641  infpnlem1  12957  ramubcl  13065  ressress  13205  mreexmrid  13545  gsum2d  15223  ablfacrplem  15300  mplsubrglem  16183  infil  17558  fbasfip  17563  fgcl  17573  fin1aufil  17627  hauspwpwf1  17682  ovolicc2lem4  18879  ovolioo  18925  i1fima2sn  19035  itg1addlem4  19054  itgsplitioo  19192  lhop1lem  19360  chordthmlem  20129  ressatans  20230  ftalem5  20314  ppiprm  20389  chtprm  20391  lgsdir2lem2  20563  dirith2  20677  ballotlemfp1  23050  erdszelem8  23729  nodenselem7  24341  nobndup  24354  nobnddown  24355  axlowdimlem13  24582  axlowdim1  24587  nandsym1  24861  onsucsuccmpi  24882  onint1  24888  areacirclem5  24929  intn3an1d  24936  intn3an2d  24937  intn3an3d  24938  nn0prpwlem  26238  nn0prpw  26239  ivthALT  26258  prtlem90  26723  irrapx1  26913  hdmaplem1  31961  hdmaplem2N  31962  hdmaplem3  31963
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator