Theorem mtand 665

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 663	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 614  ax-in2 615

This theorem is referenced by:  frirrg  4352  phpm  6867  diffisn  6895  tridc  6901  nnnninfeq  7128  pm54.43  7191  addcanprleml  7615  addcanprlemu  7616  iseqf1olemklt  10487  isprm5lem  12143  pw2dvdseulemle  12169  sqne2sq  12179  pythagtriplem4  12270  pythagtriplem11  12276  pythagtriplem13  12278  ctinfomlemom  12430  lssvancl1  13459  ivthinc  14206  pwle2  14833