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  4382  phpm  6923  diffisn  6951  tridc  6957  nnnninfeq  7189  pm54.43  7252  addcanprleml  7676  addcanprlemu  7677  iseqf1olemklt  10572  isprm5lem  12282  pw2dvdseulemle  12308  sqne2sq  12318  pythagtriplem4  12409  pythagtriplem11  12415  pythagtriplem13  12417  ctinfomlemom  12587  rrgnz  13767  lssvancl1  13866  ivthinc  14822  pwle2  15559