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  2412  cesaro  2416  pwnss  4612  reusv2lem2  4649  reldmtpos  6960  tz7.49  7107  omopthlem2  7302  domnsym  7640  sdomirr  7651  infensuc  7692  fofinf1o  7797  elfi2  7870  sucprcregOLD  8022  infdifsn  8069  carden2b  8344  alephsucdom  8456  infdif2  8586  fin4i  8674  bitsf1  13951  pcmpt2  14267  ufinffr  20165  chtub  23215  eupath2lem1  24653  gxnval  24938  oddpwdc  27933  eldmgm  28204  lgamucov  28220  facgam  28248  erdszelem10  28284  heiborlem1  29910  fphpd  30354  usgedgnlp  31879  bnj1312  33193  osumcllem4N  34755  pexmidlem1N  34766
  Copyright terms: Public domain W3C validator