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  1944  oprcl  3899  tfi  4723  limom  4750  ovrcl  5972  oaabs2  6727  ecexr  6749  elpmi  6874  elmapex  6876  pmresg  6880  pmsspw  6887  ixpssmap2g  6930  ixpssmapg  6931  resixpfo  6939  infensuc  7124  pm54.43lem  7719  alephnbtwn  7785  cfpwsdom  8293  elbasfv  13282  elbasov  13283  restsspw  13429  isipodrs  14357  grpidval  14477  efgrelexlema  15151  subcmn  15226  dvdsrval  15520  mvrf1  16263  psr1rclOLD  16372  ply1rclOLD  16375  elocv  16668  tgclb  16808  restrcl  16988  ssrest  17007  iscnp2  17069  isfcls  17800  isnghm  18328  pf1rcl  19530  dchrrcl  20585  hmdmadj  22628  indispcon  24169  cvmtop1  24195  cvmtop2  24196  dfon2lem7  24703  sltval2  24868  sltres  24876  eleenn  25083  rankeq1o  25360  mapco2g  26113  matrcl  26789  dvelimvNEW7  28868  atbase  29531  llnbase  29750  lplnbase  29775  lvolbase  29819  lhpbase  30239
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator