Theorem mtand 666

Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypotheses

Ref	Expression
mtand.1	|- ( ph -> -. ch )
mtand.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mtand	|- ( ph -> -. ps )

Proof of Theorem mtand

Step	Hyp	Ref	Expression
1		mtand.1	. 2 |- ( ph -> -. ch )
2		mtand.2	. . 3 |- ( ( ph /\ ps ) -> ch )
3	2	ex 115	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtod 664	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem is referenced by:  frirrg  4396  phpm  6961  diffisn  6989  tridc  6995  nnnninfeq  7229  pm54.43  7297  addcanprleml  7726  addcanprlemu  7727  iseqf1olemklt  10641  isprm5lem  12434  pw2dvdseulemle  12460  sqne2sq  12470  pythagtriplem4  12562  pythagtriplem11  12568  pythagtriplem13  12570  ctinfomlemom  12769  rrgnz  14001  lssvancl1  14100  ivthinc  15086  pwle2  15897  nninfnfiinf  15922