Theorem mtand 667

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 665	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  4415  phpm  6988  diffisn  7016  tridc  7022  nnnninfeq  7256  pm54.43  7324  addcanprleml  7762  addcanprlemu  7763  iseqf1olemklt  10680  isprm5lem  12578  pw2dvdseulemle  12604  sqne2sq  12614  pythagtriplem4  12706  pythagtriplem11  12712  pythagtriplem13  12714  ctinfomlemom  12913  rrgnz  14145  lssvancl1  14244  ivthinc  15230  pwle2  16137  nninfnfiinf  16162