Theorem nsyl 628

Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)

Hypotheses

Ref	Expression
nsyl.1	|- ( ph -> -. ps )
nsyl.2	|- ( ch -> ps )

Assertion

Ref	Expression
nsyl	|- ( ph -> -. ch )

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 |- ( ph -> -. ps )
2		nsyl.2	. . 3 |- ( ch -> ps )
3	1, 2	nsyl3 626	. 2 |- ( ch -> -. ph )
4	3	con2i 627	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 614  ax-in2 615

This theorem is referenced by:  con3i  632  pm4.52im  750  intnand  931  intnanrd  932  camestres  2129  camestros  2133  calemes  2140  calemos  2143  unssin  3372  inssun  3373  onsucelsucexmid  4523  funun  5252  pwuninel2  6273  swoer  6553  swoord1  6554  swoord2  6555  ssfirab  6923  djune  7067  exmidaclem  7197  sucpw1nss3  7224  onntri35  7226  onntri45  7230  elnnz  9234  lbioog  9882  ubioog  9883  fzneuz  10069  fzodisj  10146  fxnn0nninf  10406  zfz1isolemiso  10785  infssuzex  11915  infpnlem1  12322  exmidunben  12392  lgsdir2lem2  13999