Theorem mtod 665

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 662	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  666  mtand  667  mtbid  674  mtbird  675  pwntru  4254  po2nr  4369  po3nr  4370  sotricim  4383  elirr  4602  ordn2lp  4606  en2lp  4615  tfr1onlemsucaccv  6445  tfrcllemsucaccv  6458  nndomo  6981  fnfi  7059  difinfsnlem  7222  nninfwlpoimlemginf  7299  2omotaplemap  7399  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  caucvgprlemladdrl  7821  caucvgprprlemaddq  7851  msqge0  8719  mulge0  8722  squeeze0  9007  elnn0z  9415  fznlem  10193  frec2uzf1od  10583  seqf1oglem1  10696  facndiv  10916  sumrbdclem  11773  prodrbdclem  11967  alzdvds  12250  fzm1ndvds  12252  fzo0dvdseq  12253  bitsfzolem  12350  bitsfzo  12351  rpdvds  12506  nonsq  12614  prmdiv  12642  odzdvds  12653  pcprendvds  12698  pcprendvds2  12699  pcpremul  12701  pcdvdsb  12728  pcadd2  12749  pockthlem  12764  1arith  12775  4sqlem11  12809  4sqlem17  12815  ennnfonelemim  12880  bldisj  14958  perfect1  15555  lgsdilem2  15598  lgsne0  15600  lgseisenlem1  15632  lgseisenlem2  15633  lgsquadlem1  15639  lgsquadlem2  15640  lgsquadlem3  15641  lgsquad2lem1  15643  bj-nnen2lp  16059  pwtrufal  16106  refeq  16139