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  757  intnand  938  intnanrd  939  intn3an1d  1392  intn3an2d  1393  intn3an3d  1394  camestres  2185  camestros  2189  calemes  2196  calemos  2199  unssin  3446  inssun  3447  onsucelsucexmid  4628  funun  5371  opabn1stprc  6357  pwuninel2  6447  swoer  6729  swoord1  6730  swoord2  6731  ssfirab  7128  djune  7276  exmidaclem  7422  sucpw1nss3  7452  onntri35  7454  onntri45  7458  elnnz  9488  lbioog  10147  ubioog  10148  fzneuz  10335  fzodisj  10414  fzodisjsn  10418  infssuzex  10492  fxnn0nninf  10700  zfz1isolemiso  11102  swrd0g  11240  infpnlem1  12931  exmidunben  13046  lgsdir2lem2  15757  2lgslem3  15829  vdegp1aid  16164