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  2219  cesaro  2223  reusv2lem2  4473  reldmtpos  6141  pwnss  6230  tz7.49  6390  omopthlem2  6587  domnsym  6920  sdomirr  6931  infensuc  6972  fofinf1o  7070  elfi2  7101  sucprcreg  7246  infdifsn  7290  carden2b  7533  alephsucdom  7639  infdif2  7769  fin4i  7857  rpnnen2lem9  12428  bitsf1  12564  pcmpt2  12868  ramub1lem1  13000  ramub1lem2  13001  ufinffr  17551  chtub  20378  gxnval  20852  eldmgm  23031  erdszelem10  23068  eupath2lem1  23238  heiborlem1  25867  fphpd  26231  bnj1312  28100  ax9X  28232  ax9vax9  28288  osumcllem4N  29278  pexmidlem1N  29289
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator