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  2188  camestros  2192  calemes  2199  calemos  2202  unssin  3464  inssun  3465  onsucelsucexmid  4659  funun  5404  opabn1stprc  6404  pwuninel2  6528  swoer  6810  swoord1  6811  swoord2  6812  ssfirab  7212  djune  7384  exmidaclem  7530  sucpw1nss3  7560  onntri35  7562  onntri45  7566  elnnz  9609  lbioog  10270  ubioog  10271  fzneuz  10462  fzodisj  10541  fzodisjsn  10545  infssuzex  10620  fxnn0nninf  10830  zfz1isolemiso  11241  swrd0g  11382  infpnlem1  13088  ballotfilemfp1  13181  ballotfilem4  13191  ballotfilemirc  13225  exmidunben  13267  lgsdir2lem2  16033  2lgslem3  16105  vdegp1aid  16440