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

Theorem nsyl2 119
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 10 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mt3d 117 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con1i  121  con4i  122  dvelimv  1892  oprcl  3836  tfi  4660  limom  4687  ovrcl  5904  oaabs2  6659  ecexr  6681  elpmi  6805  elmapex  6807  pmresg  6811  pmsspw  6818  ixpssmap2g  6861  ixpssmapg  6862  resixpfo  6870  infensuc  7055  pm54.43lem  7648  alephnbtwn  7714  cfpwsdom  8222  elbasfv  13207  elbasov  13208  restsspw  13352  isipodrs  14280  grpidval  14400  efgrelexlema  15074  subcmn  15149  dvdsrval  15443  mvrf1  16186  psr1rclOLD  16295  ply1rclOLD  16298  elocv  16584  tgclb  16724  restrcl  16904  ssrest  16923  iscnp2  16985  isfcls  17720  isnghm  18248  pf1rcl  19448  dchrrcl  20495  hmdmadj  22536  indispcon  23780  cvmtop1  23806  cvmtop2  23807  dfon2lem7  24216  sltval2  24381  sltres  24389  eleenn  24596  rankeq1o  24873  mapco2g  26893  matrcl  27569  dvelimvNEW7  29439  atbase  30101  llnbase  30320  lplnbase  30345  lvolbase  30389  lhpbase  30809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator