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 12 . 2  |-  ( ch 
->  ( ph  ->  -.  ps ) )
41, 3mt2d 111 1  |-  ( ch 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  con2i  114  nsyl  115  ax9  1683  cesare  2216  cesaro  2220  reusv2lem2  4427  reldmtpos  6094  pwnss  6183  tz7.49  6343  omopthlem2  6540  domnsym  6872  sdomirr  6883  infensuc  6924  fofinf1o  7022  elfi2  7052  sucprcreg  7197  infdifsn  7241  carden2b  7484  alephsucdom  7590  infdif2  7720  fin4i  7808  rpnnen2lem9  12375  bitsf1  12511  pcmpt2  12815  ramub1lem1  12947  ramub1lem2  12948  ufinffr  17456  chtub  20283  gxnval  20757  eldmgm  22865  erdszelem10  22902  eupath2lem1  23072  heiborlem1  25701  fphpd  26065  bnj1312  27777  ax9vax9  27847  osumcllem4N  28837  pexmidlem1N  28848
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator