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  1879  oprcl  3820  tfi  4644  limom  4671  ovrcl  5888  oaabs2  6643  ecexr  6665  elpmi  6789  elmapex  6791  pmresg  6795  pmsspw  6802  ixpssmap2g  6845  ixpssmapg  6846  resixpfo  6854  infensuc  7039  pm54.43lem  7632  alephnbtwn  7698  cfpwsdom  8206  elbasfv  13191  elbasov  13192  restsspw  13336  isipodrs  14264  grpidval  14384  efgrelexlema  15058  subcmn  15133  dvdsrval  15427  mvrf1  16170  psr1rclOLD  16279  ply1rclOLD  16282  elocv  16568  tgclb  16708  restrcl  16888  ssrest  16907  iscnp2  16969  isfcls  17704  isnghm  18232  pf1rcl  19432  dchrrcl  20479  hmdmadj  22520  indispcon  23765  cvmtop1  23791  cvmtop2  23792  dfon2lem7  24145  sltval2  24310  sltres  24318  eleenn  24524  rankeq1o  24801  mapco2g  26790  matrcl  27466  atbase  29479  llnbase  29698  lplnbase  29723  lvolbase  29767  lhpbase  30187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator