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  12405  pw2dvdseulemle  12431  sqne2sq  12441  pythagtriplem4  12533  pythagtriplem11  12539  pythagtriplem13  12541  ctinfomlemom  12740  rrgnz  13972  lssvancl1  14071  ivthinc  15057  pwle2  15868  nninfnfiinf  15893