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  4453  phpm  7095  diffisn  7125  tridc  7132  nnnninfeq  7370  pm54.43  7438  addcanprleml  7877  addcanprlemu  7878  iseqf1olemklt  10806  isprm5lem  12776  pw2dvdseulemle  12802  sqne2sq  12812  pythagtriplem4  12904  pythagtriplem11  12910  pythagtriplem13  12912  ctinfomlemom  13111  rrgnz  14347  lssvancl1  14446  ivthinc  15437  g0wlk0  16294  pwle2  16703  nninfnfiinf  16732