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  4476  phpm  7133  diffisn  7163  tridc  7170  nnnninfeq  7432  pm54.43  7500  addcanprleml  7945  addcanprlemu  7946  iseqf1olemklt  10884  sshashneg  11230  isprm5lem  12863  pw2dvdseulemle  12889  sqne2sq  12899  pythagtriplem4  12991  pythagtriplem11  12997  pythagtriplem13  12999  ballotfilemfcc  13177  ballotfilemi1  13189  ballotfilemii  13190  ctinfomlemom  13262  rrgnz  14515  lssvancl1  14641  ivthinc  15634  g0wlk0  16491  pwle2  16898  nninfnfiinf  16927