Theorem mtand 520

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 402	. 2 |- (ph -> (ps -> ch))
4	1, 3	mtod 123	1 |- (ph -> -. ps)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240

This theorem is referenced by:  peano5 3975  sdomnsym 5525  ondomcard 6009  lmle 9238  efif1lem5 10088  wfrlem16 13972  nocvxminlem 14028  axfelem15 14045  reconnlem5 15450  isufil2 15565  ufileu 15573  bfplem9 16006

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain