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  7051  diffisn  7081  tridc  7088  nnnninfeq  7326  pm54.43  7394  addcanprleml  7833  addcanprlemu  7834  iseqf1olemklt  10759  isprm5lem  12712  pw2dvdseulemle  12738  sqne2sq  12748  pythagtriplem4  12840  pythagtriplem11  12846  pythagtriplem13  12848  ctinfomlemom  13047  rrgnz  14281  lssvancl1  14380  ivthinc  15366  g0wlk0  16220  pwle2  16599  nninfnfiinf  16625