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  10948  sshashneg  11295  isprm5lem  12936  pwbdvdseulemle  12962  sqne2sq  12973  pythagtriplem4  13067  pythagtriplem11  13073  pythagtriplem13  13075  ballotfilemfcc  13282  ballotfilemi1  13294  ballotfilemii  13295  ctinfomlemom  13367  rrgnz  14626  lssvancl1  14753  ivthinc  15793  g0wlk0  16709  pwle2  17126  nninfnfiinf  17164