Theorem nsyl3 635

Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)

Hypotheses

Ref	Expression
nsyl3.1	|- ( ph -> -. ps )
nsyl3.2	|- ( ch -> ps )

Assertion

Ref	Expression
nsyl3	|- ( ch -> -. ph )

Proof of Theorem nsyl3

Step	Hyp	Ref	Expression
1		nsyl3.2	. 2 |- ( ch -> ps )
2		nsyl3.1	. . 3 |- ( ph -> -. ps )
3	2	a1i 9	. 2 |- ( ch -> ( ph -> -. ps ) )
4	1, 3	mt2d 634	1 |- ( ch -> -. ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is referenced by:  con2i  636  nsyl  637  pm2.65i  648  cesare  2191  cesaro  2195  pwnss  4291  sucprcreg  4691  reg3exmidlemwe  4721  reldmtpos  6514  snexxph  7257  elfi2  7296  ismkvnex  7485  fzn  10425  seq3f1olemqsum  10928  pcmpt2  13101  elply2  15759  umgredgnlp  16307  clwwlkn0  16563