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  2397  cesaro  2401  pwnss  4558  reusv2lem2  4595  reldmtpos  6856  tz7.49  7003  omopthlem2  7198  domnsym  7540  sdomirr  7551  infensuc  7592  fofinf1o  7696  elfi2  7768  sucprcregOLD  7919  infdifsn  7966  carden2b  8241  alephsucdom  8353  infdif2  8483  fin4i  8571  bitsf1  13753  pcmpt2  14066  ufinffr  19627  chtub  22677  eupath2lem1  23743  gxnval  23892  oddpwdc  26874  eldmgm  27145  lgamucov  27161  facgam  27189  erdszelem10  27225  heiborlem1  28851  fphpd  29296  bnj1312  32352  osumcllem4N  33912  pexmidlem1N  33923
  Copyright terms: Public domain W3C validator