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

Theorem nsyl3 113
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 111 1  |-  ( ch 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con2i  114  nsyl  115  ax9OLD  1991  cesare  2342  cesaro  2346  pwnss  4307  reusv2lem2  4666  reldmtpos  6424  tz7.49  6639  omopthlem2  6836  domnsym  7170  sdomirr  7181  infensuc  7222  fofinf1o  7324  elfi2  7355  sucprcreg  7501  infdifsn  7545  carden2b  7788  alephsucdom  7894  infdif2  8024  fin4i  8112  bitsf1  12886  pcmpt2  13190  ufinffr  17883  chtub  20864  eupath2lem1  21548  gxnval  21697  eldmgm  24586  lgamucov  24602  facgam  24630  erdszelem10  24666  heiborlem1  26212  fphpd  26569  bnj1312  28766  ax9NEW7  28807  osumcllem4N  30074  pexmidlem1N  30085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator