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  1891  cesare  2248  cesaro  2252  reusv2lem2  4536  reldmtpos  6204  pwnss  6293  tz7.49  6453  omopthlem2  6650  domnsym  6983  sdomirr  6994  infensuc  7035  fofinf1o  7133  elfi2  7164  sucprcreg  7309  infdifsn  7353  carden2b  7596  alephsucdom  7702  infdif2  7832  fin4i  7920  rpnnen2lem9  12496  bitsf1  12632  pcmpt2  12936  ramub1lem1  13068  ramub1lem2  13069  ufinffr  17619  chtub  20446  gxnval  20920  eldmgm  23099  erdszelem10  23136  eupath2lem1  23306  heiborlem1  25935  fphpd  26299  bnj1312  28356  ax9vax9  28426  osumcllem4N  29416  pexmidlem1N  29427
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator