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 11 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mt3d 119 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con1i  123  con4i  124  dvelimvOLD  1985  oprcl  3950  tfi  4773  limom  4800  ovrcl  6050  oaabs2  6824  ecexr  6846  elpmi  6971  elmapex  6973  pmresg  6977  pmsspw  6984  ixpssmap2g  7027  ixpssmapg  7028  resixpfo  7036  infensuc  7221  pm54.43lem  7819  alephnbtwn  7885  cfpwsdom  8392  elbasfv  13439  elbasov  13440  restsspw  13586  homarcl  14110  isipodrs  14514  grpidval  14634  efgrelexlema  15308  subcmn  15383  dvdsrval  15677  mvrf1  16416  elocv  16818  restrcl  17143  ssrest  17162  iscnp2  17225  isfcls  17962  isnghm  18628  pf1rcl  19836  dchrrcl  20891  hmdmadj  23291  indispcon  24700  cvmtop1  24726  cvmtop2  24727  dfon2lem7  25169  sltval2  25334  sltres  25342  funpartlem  25505  eleenn  25549  rankeq1o  25826  mapco2g  26460  matrcl  27135  dvelimvNEW7  28800  atbase  29404  llnbase  29623  lplnbase  29648  lvolbase  29692  lhpbase  30112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator