Theorem mtod 588

Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mtod.1	|- (ph -> -. ch)
mtod.2	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
mtod	|- (ph -> -. ps)

Proof of Theorem mtod

Step	Hyp	Ref	Expression
1		mtod.2	. 2 |- (ph -> (ps -> ch))
2		mtod.1	. . 3 |- (ph -> -. ch)
3	2	a1d 22	. 2 |- (ph -> (ps -> -. ch))
4	1, 3	pm2.65d 585	1 |- (ph -> -. ps)

Syntax hints:  -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 544  ax-in2 545

This theorem is referenced by:  mtoi  589  mtand  590  mtbid  596  mtbird  597  po2nr  4037  po3nr  4038  sotricim  4051  elirr  4224  en2lp  4232  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  msqge0  7400  mulge0  7403  squeeze0  7651  elnn0z  8034  fznlem  8675  frec2uzf1od  8873  bj-nnen2lp  9414