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  7173  diffisn  7203  tridc  7210  nnnninfeq  7474  pm54.43  7542  addcanprleml  7987  addcanprlemu  7988  iseqf1olemklt  10955  sshashneg  11302  isprm5lem  12944  pwbdvdseulemle  12970  sqne2sq  12981  pythagtriplem4  13075  pythagtriplem11  13081  pythagtriplem13  13083  ballotfilemfcc  13290  ballotfilemi1  13302  ballotfilemii  13303  ctinfomlemom  13375  rrgnz  14685  lssvancl1  14812  ivthinc  15886  g0wlk0  16833  pwle2  17250  nninfnfiinf  17289