Theorem mtand 669

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 667	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 617  ax-in2 618

This theorem is referenced by:  frirrg  4445  phpm  7047  diffisn  7075  tridc  7082  nnnninfeq  7318  pm54.43  7386  addcanprleml  7824  addcanprlemu  7825  iseqf1olemklt  10750  isprm5lem  12703  pw2dvdseulemle  12729  sqne2sq  12739  pythagtriplem4  12831  pythagtriplem11  12837  pythagtriplem13  12839  ctinfomlemom  13038  rrgnz  14272  lssvancl1  14371  ivthinc  15357  g0wlk0  16167  pwle2  16535  nninfnfiinf  16561