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  1889  cesare  2246  cesaro  2250  pwnss  4176  reusv2lem2  4536  reldmtpos  6242  tz7.49  6457  omopthlem2  6654  domnsym  6987  sdomirr  6998  infensuc  7039  fofinf1o  7137  elfi2  7168  sucprcreg  7313  infdifsn  7357  carden2b  7600  alephsucdom  7706  infdif2  7836  fin4i  7924  rpnnen2lem9  12501  bitsf1  12637  pcmpt2  12941  ramub1lem1  13073  ramub1lem2  13074  ufinffr  17624  chtub  20451  gxnval  20927  eldmgm  23694  erdszelem10  23731  eupath2lem1  23901  heiborlem1  26535  fphpd  26899  bnj1312  29088  ax9vax9  29158  osumcllem4N  30148  pexmidlem1N  30159
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator