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 11 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mt3d 119 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con1i  123  con4i  124  dvelimvOLD  2028  oprcl  3995  tfi  4819  limom  4846  ovrcl  6097  oaabs2  6874  ecexr  6896  elpmi  7021  elmapex  7023  pmresg  7027  pmsspw  7034  ixpssmap2g  7077  ixpssmapg  7078  resixpfo  7086  infensuc  7271  pm54.43lem  7870  alephnbtwn  7936  cfpwsdom  8443  elbasfv  13495  elbasov  13496  restsspw  13642  homarcl  14166  isipodrs  14570  grpidval  14690  efgrelexlema  15364  subcmn  15439  dvdsrval  15733  mvrf1  16472  elocv  16878  restrcl  17204  ssrest  17223  iscnp2  17286  isfcls  18024  isnghm  18740  pf1rcl  19952  dchrrcl  21007  hmdmadj  23426  indispcon  24904  cvmtop1  24930  cvmtop2  24931  dfon2lem7  25395  sltval2  25560  sltres  25568  funpartlem  25732  eleenn  25778  rankeq1o  26055  mapco2g  26701  matrcl  27376  dvelimvNEW7  29214  atbase  29818  llnbase  30037  lplnbase  30062  lvolbase  30106  lhpbase  30526
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator