Theorem mtod 625

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 622	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 580  ax-in2 581

This theorem is referenced by:  mtoi  626  mtand  627  mtbid  633  mtbird  634  po2nr  4145  po3nr  4146  sotricim  4159  elirr  4370  ordn2lp  4374  en2lp  4383  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  nndomo  6634  fnfi  6700  cauappcvgprlemladdru  7269  cauappcvgprlemladdrl  7270  caucvgprlemladdrl  7291  caucvgprprlemaddq  7321  msqge0  8147  mulge0  8150  squeeze0  8419  elnn0z  8817  fznlem  9509  frec2uzf1od  9867  facndiv  10201  isumrblem  10819  alzdvds  11187  fzm1ndvds  11189  fzo0dvdseq  11190  rpdvds  11413  nonsq  11517  bj-nnen2lp  12115