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  4440  phpm  7023  diffisn  7051  tridc  7057  nnnninfeq  7291  pm54.43  7359  addcanprleml  7797  addcanprlemu  7798  iseqf1olemklt  10715  isprm5lem  12658  pw2dvdseulemle  12684  sqne2sq  12694  pythagtriplem4  12786  pythagtriplem11  12792  pythagtriplem13  12794  ctinfomlemom  12993  rrgnz  14226  lssvancl1  14325  ivthinc  15311  pwle2  16323  nninfnfiinf  16348