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

Theorem nsyl3 111
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 10 . 2  |-  ( ch 
->  ( ph  ->  -.  ps ) )
41, 3mt2d 109 1  |-  ( ch 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con2i  112  nsyl  113  ax9  1902  cesare  2259  cesaro  2263  pwnss  4192  reusv2lem2  4552  reldmtpos  6258  tz7.49  6473  omopthlem2  6670  domnsym  7003  sdomirr  7014  infensuc  7055  fofinf1o  7153  elfi2  7184  sucprcreg  7329  infdifsn  7373  carden2b  7616  alephsucdom  7722  infdif2  7852  fin4i  7940  rpnnen2lem9  12517  bitsf1  12653  pcmpt2  12957  ramub1lem1  13089  ramub1lem2  13090  ufinffr  17640  chtub  20467  gxnval  20943  eldmgm  23709  erdszelem10  23746  eupath2lem1  23916  heiborlem1  26638  fphpd  27002  bnj1312  29404  ax9NEW7  29445  ax9vax9  29780  osumcllem4N  30770  pexmidlem1N  30781
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator