Theorem nsyl 633

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 631	. 2 |- ( ch -> -. ph )
4	3	con2i 632	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 619  ax-in2 620

This theorem is referenced by:  con3i  637  pm4.52im  758  intnand  939  intnanrd  940  intn3an1d  1393  intn3an2d  1394  intn3an3d  1395  camestres  2186  camestros  2190  calemes  2197  calemos  2200  unssin  3460  inssun  3461  onsucelsucexmid  4652  funun  5397  opabn1stprc  6389  pwuninel2  6513  swoer  6795  swoord1  6796  swoord2  6797  ssfirab  7197  djune  7369  exmidaclem  7515  sucpw1nss3  7545  onntri35  7547  onntri45  7551  elnnz  9587  lbioog  10246  ubioog  10247  fzneuz  10435  fzodisj  10514  fzodisjsn  10518  infssuzex  10593  fxnn0nninf  10801  zfz1isolemiso  11211  swrd0g  11352  infpnlem1  13057  exmidunben  13177  lgsdir2lem2  15902  2lgslem3  15974  vdegp1aid  16309