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  2185  camestros  2189  calemes  2196  calemos  2199  unssin  3448  inssun  3449  onsucelsucexmid  4634  funun  5378  opabn1stprc  6367  pwuninel2  6491  swoer  6773  swoord1  6774  swoord2  6775  ssfirab  7172  djune  7337  exmidaclem  7483  sucpw1nss3  7513  onntri35  7515  onntri45  7519  elnnz  9550  lbioog  10209  ubioog  10210  fzneuz  10398  fzodisj  10477  fzodisjsn  10481  infssuzex  10556  fxnn0nninf  10764  zfz1isolemiso  11166  swrd0g  11307  infpnlem1  13012  exmidunben  13127  lgsdir2lem2  15848  2lgslem3  15920  vdegp1aid  16255