Theorem nsyl3 631

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 630	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 619  ax-in2 620

This theorem is referenced by:  con2i  632  nsyl  633  pm2.65i  644  cesare  2184  cesaro  2188  pwnss  4249  sucprcreg  4647  reg3exmidlemwe  4677  reldmtpos  6419  snexxph  7149  elfi2  7171  ismkvnex  7354  fzn  10277  seq3f1olemqsum  10776  pcmpt2  12935  elply2  15478  umgredgnlp  16022  clwwlkn0  16278