Theorem mtod 621

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 618	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 576  ax-in2 577

This theorem is referenced by:  mtoi  622  mtand  623  mtbid  629  mtbird  630  po2nr  4064  po3nr  4065  sotricim  4078  elirr  4284  ordn2lp  4288  en2lp  4297  nndomo  6350  fnfi  6388  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  caucvgprprlemaddq  6898  msqge0  7716  mulge0  7719  squeeze0  7982  elnn0z  8364  fznlem  9060  frec2uzf1od  9408  facndiv  9666  alzdvds  10254  fzm1ndvds  10256  fzo0dvdseq  10257  rpdvds  10481  bj-nnen2lp  10749