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  7469  pm54.43  7537  addcanprleml  7982  addcanprlemu  7983  iseqf1olemklt  10950  sshashneg  11297  isprm5lem  12939  pwbdvdseulemle  12965  sqne2sq  12976  pythagtriplem4  13070  pythagtriplem11  13076  pythagtriplem13  13078  ballotfilemfcc  13285  ballotfilemi1  13297  ballotfilemii  13298  ctinfomlemom  13370  rrgnz  14661  lssvancl1  14788  ivthinc  15835  g0wlk0  16777  pwle2  17194  nninfnfiinf  17232