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  1999  cesare  2357  cesaro  2361  pwnss  4325  reusv2lem2  4684  reldmtpos  6446  tz7.49  6661  omopthlem2  6858  domnsym  7192  sdomirr  7203  infensuc  7244  fofinf1o  7346  elfi2  7377  sucprcreg  7523  infdifsn  7567  carden2b  7810  alephsucdom  7916  infdif2  8046  fin4i  8134  bitsf1  12913  pcmpt2  13217  ufinffr  17914  chtub  20949  eupath2lem1  21652  gxnval  21801  eldmgm  24759  lgamucov  24775  facgam  24803  erdszelem10  24839  heiborlem1  26410  fphpd  26767  bnj1312  29133  ax9NEW7  29174  osumcllem4N  30441  pexmidlem1N  30452
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator