Theorem mtand 667

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 665	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 615  ax-in2 616

This theorem is referenced by:  frirrg  4410  phpm  6983  diffisn  7011  tridc  7017  nnnninfeq  7251  pm54.43  7319  addcanprleml  7757  addcanprlemu  7758  iseqf1olemklt  10675  isprm5lem  12548  pw2dvdseulemle  12574  sqne2sq  12584  pythagtriplem4  12676  pythagtriplem11  12682  pythagtriplem13  12684  ctinfomlemom  12883  rrgnz  14115  lssvancl1  14214  ivthinc  15200  pwle2  16107  nninfnfiinf  16132