Theorem mtod 664

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 661	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  mtoi  665  mtand  666  mtbid  673  mtbird  674  pwntru  4211  po2nr  4321  po3nr  4322  sotricim  4335  elirr  4552  ordn2lp  4556  en2lp  4565  tfr1onlemsucaccv  6356  tfrcllemsucaccv  6369  nndomo  6878  fnfi  6950  difinfsnlem  7112  nninfwlpoimlemginf  7188  2omotaplemap  7270  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  caucvgprlemladdrl  7691  caucvgprprlemaddq  7721  msqge0  8587  mulge0  8590  squeeze0  8875  elnn0z  9280  fznlem  10055  frec2uzf1od  10420  facndiv  10733  sumrbdclem  11399  prodrbdclem  11593  alzdvds  11874  fzm1ndvds  11876  fzo0dvdseq  11877  rpdvds  12113  nonsq  12221  prmdiv  12249  odzdvds  12259  pcprendvds  12304  pcprendvds2  12305  pcpremul  12307  pcdvdsb  12333  pockthlem  12368  1arith  12379  ennnfonelemim  12439  bldisj  14254  lgsdilem2  14790  lgsne0  14792  lgseisenlem1  14803  lgseisenlem2  14804  bj-nnen2lp  15059  pwtrufal  15101  refeq  15130