MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyl3 Structured version   Unicode version

Theorem nsyl3 119
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 117 1  |-  ( ch 
->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con2i  120  nsyl  121  cesare  2386  cesaro  2390  pwnss  4452  reusv2lem2  4489  reldmtpos  6748  tz7.49  6892  omopthlem2  7087  domnsym  7429  sdomirr  7440  infensuc  7481  fofinf1o  7584  elfi2  7656  sucprcregOLD  7807  infdifsn  7854  carden2b  8129  alephsucdom  8241  infdif2  8371  fin4i  8459  bitsf1  13634  pcmpt2  13947  ufinffr  19477  chtub  22526  eupath2lem1  23549  gxnval  23698  oddpwdc  26689  eldmgm  26960  lgamucov  26976  facgam  27004  erdszelem10  27040  heiborlem1  28663  fphpd  29108  bnj1312  31936  osumcllem4N  33443  pexmidlem1N  33454
  Copyright terms: Public domain W3C validator