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  2187  cesaro  2191  pwnss  4277  sucprcreg  4676  reg3exmidlemwe  4706  reldmtpos  6497  snexxph  7233  elfi2  7272  ismkvnex  7459  fzn  10396  seq3f1olemqsum  10899  pcmpt2  13067  elply2  15726  umgredgnlp  16273  clwwlkn0  16529