Theorem mtand 655

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 114	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtod 653	1 |- ( ph -> -. ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem is referenced by:  frirrg  4327  phpm  6827  diffisn  6855  tridc  6861  nnnninfeq  7088  pm54.43  7142  addcanprleml  7551  addcanprlemu  7552  iseqf1olemklt  10416  isprm5lem  12069  pw2dvdseulemle  12095  sqne2sq  12105  pythagtriplem4  12196  pythagtriplem11  12202  pythagtriplem13  12204  ctinfomlemom  12356  ivthinc  13221  pwle2  13838