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

Theorem nsyl3 119
Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
Hypotheses
Ref Expression
nsyl3.1  |-  ( ph  ->  -.  ps )
nsyl3.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
nsyl3  |-  ( ch 
->  -.  ph )

Proof of Theorem nsyl3
StepHypRef Expression
1 nsyl3.2 . 2  |-  ( ch 
->  ps )
2 nsyl3.1 . . 3  |-  ( ph  ->  -.  ps )
32a1i 11 . 2  |-  ( ch 
->  ( ph  ->  -.  ps ) )
41, 3mt2d 117 1  |-  ( ch 
->  -.  ph )
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:  con2i  120  nsyl  121  cesare  2399  cesaro  2403  pwnss  4602  reusv2lem2  4639  reldmtpos  6955  tz7.49  7102  omopthlem2  7297  domnsym  7636  sdomirr  7647  infensuc  7688  fofinf1o  7793  elfi2  7866  infdifsn  8064  carden2b  8339  alephsucdom  8451  infdif2  8581  fin4i  8669  bitsf1  14183  pcmpt2  14499  ufinffr  20599  chtub  23688  eupath2lem1  25182  gxnval  25463  oddpwdc  28560  eldmgm  28831  lgamucov  28847  facgam  28875  erdszelem10  28911  heiborlem1  30550  fphpd  30992  usgedgnlp  32801  0nodd  32889  bnj1312  34534  osumcllem4N  36099  pexmidlem1N  36110
  Copyright terms: Public domain W3C validator