Theorem nsyl3 627

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 626	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 615  ax-in2 616

This theorem is referenced by:  con2i  628  nsyl  629  pm2.65i  640  cesare  2158  cesaro  2162  pwnss  4204  sucprcreg  4598  reg3exmidlemwe  4628  reldmtpos  6341  snexxph  7054  elfi2  7076  ismkvnex  7259  fzn  10166  seq3f1olemqsum  10660  pcmpt2  12700  elply2  15240