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  4364  phpm  6882  diffisn  6910  tridc  6916  nnnninfeq  7143  pm54.43  7206  addcanprleml  7630  addcanprlemu  7631  iseqf1olemklt  10502  isprm5lem  12158  pw2dvdseulemle  12184  sqne2sq  12194  pythagtriplem4  12285  pythagtriplem11  12291  pythagtriplem13  12293  ctinfomlemom  12445  lssvancl1  13643  ivthinc  14504  pwle2  15132