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  4447  phpm  7052  diffisn  7082  tridc  7089  nnnninfeq  7327  pm54.43  7395  addcanprleml  7834  addcanprlemu  7835  iseqf1olemklt  10761  isprm5lem  12731  pw2dvdseulemle  12757  sqne2sq  12767  pythagtriplem4  12859  pythagtriplem11  12865  pythagtriplem13  12867  ctinfomlemom  13066  rrgnz  14301  lssvancl1  14400  ivthinc  15386  g0wlk0  16240  pwle2  16650  nninfnfiinf  16676