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

Theorem nsyl2 121
Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)
Hypotheses
Ref Expression
nsyl2.1  |-  ( ph  ->  -.  ps )
nsyl2.2  |-  ( -. 
ch  ->  ps )
Assertion
Ref Expression
nsyl2  |-  ( ph  ->  ch )

Proof of Theorem nsyl2
StepHypRef Expression
1 nsyl2.1 . 2  |-  ( ph  ->  -.  ps )
2 nsyl2.2 . . 3  |-  ( -. 
ch  ->  ps )
32a1i 12 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mt3d 119 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  con1i  123  con4i  124  ax10lem24  1673  oprcl  3780  tfi  4602  limom  4629  ovrcl  5808  oaabs2  6597  ecexr  6619  elpmi  6743  elmapex  6745  pmresg  6749  pmsspw  6756  ixpssmap2g  6799  ixpssmapg  6800  resixpfo  6808  infensuc  6993  pm54.43lem  7586  alephnbtwn  7652  cfpwsdom  8160  elbasfv  13139  elbasov  13140  restsspw  13284  isipodrs  14212  grpidval  14332  efgrelexlema  15006  subcmn  15081  dvdsrval  15375  mvrf1  16118  psr1rclOLD  16227  ply1rclOLD  16230  elocv  16516  tgclb  16656  restrcl  16836  ssrest  16855  iscnp2  16917  isfcls  17652  isnghm  18180  pf1rcl  19380  dchrrcl  20427  hmdmadj  22466  indispcon  23123  cvmtop1  23149  cvmtop2  23150  dfon2lem7  23500  sltval2  23664  sltres  23672  eleenn  23885  rankeq1o  24162  mapco2g  26143  matrcl  26819  ax10lem24X  28244  atbase  28630  llnbase  28849  lplnbase  28874  lvolbase  28918  lhpbase  29338
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator