Theorem nsyl3 629

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 628	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 617  ax-in2 618

This theorem is referenced by:  con2i  630  nsyl  631  pm2.65i  642  cesare  2182  cesaro  2186  pwnss  4247  sucprcreg  4645  reg3exmidlemwe  4675  reldmtpos  6414  snexxph  7140  elfi2  7162  ismkvnex  7345  fzn  10267  seq3f1olemqsum  10765  pcmpt2  12907  elply2  15449  umgredgnlp  15991  clwwlkn0  16203