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  4497  phpm  7171  diffisn  7201  tridc  7208  nnnninfeq  7474  pm54.43  7542  addcanprleml  7987  addcanprlemu  7988  iseqf1olemklt  10956  sshashneg  11303  isprm5lem  12945  pwbdvdseulemle  12971  sqne2sq  12982  pythagtriplem4  13076  pythagtriplem11  13082  pythagtriplem13  13084  ballotfilemfcc  13291  ballotfilemi1  13303  ballotfilemii  13304  ctinfomlemom  13376  rrgnz  14686  lssvancl1  14813  ivthinc  15869  g0wlk0  16816  pwle2  17233  nninfnfiinf  17272