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  4441  phpm  7035  diffisn  7063  tridc  7070  nnnninfeq  7306  pm54.43  7374  addcanprleml  7812  addcanprlemu  7813  iseqf1olemklt  10732  isprm5lem  12678  pw2dvdseulemle  12704  sqne2sq  12714  pythagtriplem4  12806  pythagtriplem11  12812  pythagtriplem13  12814  ctinfomlemom  13013  rrgnz  14247  lssvancl1  14346  ivthinc  15332  g0wlk0  16111  pwle2  16423  nninfnfiinf  16449