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  dvelimv  1880  oprcl  3821  tfi  4643  limom  4670  ovrcl  5849  oaabs2  6638  ecexr  6660  elpmi  6784  elmapex  6786  pmresg  6790  pmsspw  6797  ixpssmap2g  6840  ixpssmapg  6841  resixpfo  6849  infensuc  7034  pm54.43lem  7627  alephnbtwn  7693  cfpwsdom  8201  elbasfv  13185  elbasov  13186  restsspw  13330  isipodrs  14258  grpidval  14378  efgrelexlema  15052  subcmn  15127  dvdsrval  15421  mvrf1  16164  psr1rclOLD  16273  ply1rclOLD  16276  elocv  16562  tgclb  16702  restrcl  16882  ssrest  16901  iscnp2  16963  isfcls  17698  isnghm  18226  pf1rcl  19426  dchrrcl  20473  hmdmadj  22512  indispcon  23169  cvmtop1  23195  cvmtop2  23196  dfon2lem7  23546  sltval2  23710  sltres  23718  eleenn  23931  rankeq1o  24208  mapco2g  26189  matrcl  26865  atbase  28746  llnbase  28965  lplnbase  28990  lvolbase  29034  lhpbase  29454
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator