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  23105  erdszelem10  23142  eupath2lem1  23312  heiborlem1  25947  fphpd  26311  bnj1312  28461  ax9vax9  28531  osumcllem4N  29521  pexmidlem1N  29532
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator