Theorem mtand 675

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 673	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 623  ax-in2 624

This theorem is referenced by:  frirrg  4490  phpm  7157  diffisn  7187  tridc  7194  nnnninfeq  7458  pm54.43  7526  addcanprleml  7971  addcanprlemu  7972  iseqf1olemklt  10913  sshashneg  11259  isprm5lem  12897  pw2dvdseulemle  12923  sqne2sq  12933  pythagtriplem4  13025  pythagtriplem11  13031  pythagtriplem13  13033  ballotfilemfcc  13211  ballotfilemi1  13223  ballotfilemii  13224  ctinfomlemom  13296  rrgnz  14550  lssvancl1  14676  ivthinc  15667  g0wlk0  16525  pwle2  16942  nninfnfiinf  16971