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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem is used by:  frirrg  4495  phpm  7167  diffisn  7197  tridc  7204  nnnninfeq  7468  pm54.43  7536  addcanprleml  7981  addcanprlemu  7982  iseqf1olemklt  10935  sshashneg  11281  isprm5lem  12919  pw2dvdseulemle  12945  sqne2sq  12955  pythagtriplem4  13047  pythagtriplem11  13053  pythagtriplem13  13055  ballotfilemfcc  13233  ballotfilemi1  13245  ballotfilemii  13246  ctinfomlemom  13318  rrgnz  14577  lssvancl1  14704  ivthinc  15744  g0wlk0  16611  pwle2  17028  nninfnfiinf  17066