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

Theorem nsyl2 127
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 125 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con1i  129  con4i  130  oprcl  4081  ovrcl  6120  tfi  6463  limom  6490  oaabs2  7080  ecexr  7102  elpmi  7227  elmapex  7229  pmresg  7236  pmsspw  7243  ixpssmap2g  7288  ixpssmapg  7289  resixpfo  7297  infensuc  7485  pm54.43lem  8165  alephnbtwn  8237  cfpwsdom  8744  elbasfv  14217  elbasov  14218  restsspw  14366  homarcl  14892  isipodrs  15327  grpidval  15428  efgrelexlema  16239  subcmn  16314  dvdsrval  16727  mvrf1  17476  pf1rcl  17752  elocv  18052  matrcl  18271  restrcl  18720  ssrest  18739  iscnp2  18802  isfcls  19541  isnghm  20261  dchrrcl  22538  eleenn  23077  hmdmadj  25279  indispcon  27053  cvmtop1  27079  cvmtop2  27080  dfon2lem7  27531  sltval2  27726  sltres  27734  funpartlem  27902  rankeq1o  28138  mapco2g  28975  atbase  32656  llnbase  32875  lplnbase  32900  lvolbase  32944  lhpbase  33364
  Copyright terms: Public domain W3C validator