MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyl3 Structured version   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 11 . 2  |-  ( ch 
->  ( ph  ->  -.  ps ) )
41, 3mt2d 111 1  |-  ( ch 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con2i  114  nsyl  115  ax9OLD  2033  cesare  2383  cesaro  2387  pwnss  4357  reusv2lem2  4717  reldmtpos  6479  tz7.49  6694  omopthlem2  6891  domnsym  7225  sdomirr  7236  infensuc  7277  fofinf1o  7379  elfi2  7411  sucprcreg  7557  infdifsn  7601  carden2b  7844  alephsucdom  7950  infdif2  8080  fin4i  8168  bitsf1  12948  pcmpt2  13252  ufinffr  17951  chtub  20986  eupath2lem1  21689  gxnval  21838  eldmgm  24796  lgamucov  24812  facgam  24840  erdszelem10  24876  heiborlem1  26474  fphpd  26831  bnj1312  29328  ax9NEW7  29369  osumcllem4N  30657  pexmidlem1N  30668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator