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  23176  cvmtop1  23202  cvmtop2  23203  dfon2lem7  23556  sltval2  23721  sltres  23729  eleenn  23935  rankeq1o  24212  mapco2g  26202  matrcl  26878  atbase  28852  llnbase  29071  lplnbase  29096  lvolbase  29140  lhpbase  29560
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator