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  4494  reldmtpos  6162  pwnss  6251  tz7.49  6411  omopthlem2  6608  domnsym  6941  sdomirr  6952  infensuc  6993  fofinf1o  7091  elfi2  7122  sucprcreg  7267  infdifsn  7311  carden2b  7554  alephsucdom  7660  infdif2  7790  fin4i  7878  rpnnen2lem9  12449  bitsf1  12585  pcmpt2  12889  ramub1lem1  13021  ramub1lem2  13022  ufinffr  17572  chtub  20399  gxnval  20873  eldmgm  23052  erdszelem10  23089  eupath2lem1  23259  heiborlem1  25888  fphpd  26252  bnj1312  28121  ax9X  28253  ax9vax9  28309  osumcllem4N  29299  pexmidlem1N  29310
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator