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  2131  camestros  2135  calemes  2142  calemos  2145  unssin  3374  inssun  3375  onsucelsucexmid  4527  funun  5257  pwuninel2  6278  swoer  6558  swoord1  6559  swoord2  6560  ssfirab  6928  djune  7072  exmidaclem  7202  sucpw1nss3  7229  onntri35  7231  onntri45  7235  elnnz  9257  lbioog  9907  ubioog  9908  fzneuz  10094  fzodisj  10171  fxnn0nninf  10431  zfz1isolemiso  10810  infssuzex  11940  infpnlem1  12347  exmidunben  12417  lgsdir2lem2  14212