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  6418  snexxph  7148  elfi2  7170  ismkvnex  7353  fzn  10276  seq3f1olemqsum  10774  pcmpt2  12916  elply2  15458  umgredgnlp  16002  clwwlkn0  16258