Theorem mtand 671

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 669	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 619  ax-in2 620

This theorem is referenced by:  frirrg  4471  phpm  7120  diffisn  7150  tridc  7157  nnnninfeq  7419  pm54.43  7487  addcanprleml  7929  addcanprlemu  7930  iseqf1olemklt  10860  sshashneg  11205  isprm5lem  12838  pw2dvdseulemle  12864  sqne2sq  12874  pythagtriplem4  12966  pythagtriplem11  12972  pythagtriplem13  12974  ctinfomlemom  13178  rrgnz  14414  lssvancl1  14515  ivthinc  15508  g0wlk0  16365  pwle2  16772  nninfnfiinf  16801