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

Theorem nsyl2 121
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 12 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mt3d 119 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  con1i  123  con4i  124  ax10lem24  1673  oprcl  3720  tfi  4535  limom  4562  ovrcl  5740  oaabs2  6529  ecexr  6551  elpmi  6675  elmapex  6677  pmresg  6681  pmsspw  6688  ixpssmap2g  6731  ixpssmapg  6732  resixpfo  6740  infensuc  6924  pm54.43lem  7516  alephnbtwn  7582  cfpwsdom  8086  elbasfv  13065  elbasov  13066  restsspw  13210  isipodrs  14108  grpidval  14219  efgrelexlema  14893  subcmn  14968  dvdsrval  15262  mvrf1  16002  psr1rclOLD  16111  ply1rclOLD  16114  elocv  16400  tgclb  16540  restrcl  16720  ssrest  16739  iscnp2  16801  isfcls  17536  isnghm  18064  pf1rcl  19264  dchrrcl  20311  hmdmadj  22350  indispcon  22936  cvmtop1  22962  cvmtop2  22963  dfon2lem7  23313  sltval2  23477  sltres  23485  eleenn  23698  rankeq1o  23975  mapco2g  25956  matrcl  26632  ax10lem24X  27997  atbase  28383  llnbase  28602  lplnbase  28627  lvolbase  28671  lhpbase  29091
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator