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

Theorem nsyl2 122
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 120 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con1i  124  con4i  125  dvelimvOLD  2031  oprcl  4032  tfi  4862  limom  4889  ovrcl  6140  oaabs2  6917  ecexr  6939  elpmi  7064  elmapex  7066  pmresg  7070  pmsspw  7077  ixpssmap2g  7120  ixpssmapg  7121  resixpfo  7129  infensuc  7314  pm54.43lem  7917  alephnbtwn  7983  cfpwsdom  8490  elbasfv  13543  elbasov  13544  restsspw  13690  homarcl  14214  isipodrs  14618  grpidval  14738  efgrelexlema  15412  subcmn  15487  dvdsrval  15781  mvrf1  16520  elocv  16926  restrcl  17252  ssrest  17271  iscnp2  17334  isfcls  18072  isnghm  18788  pf1rcl  20000  dchrrcl  21055  hmdmadj  23474  indispcon  24952  cvmtop1  24978  cvmtop2  24979  dfon2lem7  25447  sltval2  25642  sltres  25650  funpartlem  25818  eleenn  25866  rankeq1o  26143  mapco2g  26807  matrcl  27481  dvelimvNEW7  29560  atbase  30185  llnbase  30404  lplnbase  30429  lvolbase  30473  lhpbase  30893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator