Theorem mtod 669

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 666	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 619  ax-in2 620

This theorem is referenced by:  mtoi  670  mtand  671  mtbid  679  mtbird  680  pwntru  4295  po2nr  4412  po3nr  4413  sotricim  4426  elirr  4645  ordn2lp  4649  en2lp  4658  fvdifsuppst  6422  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  nndomo  7093  fnfi  7178  difinfsnlem  7341  nninfwlpoimlemginf  7418  2omotaplemap  7519  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprprlemaddq  7971  msqge0  8838  mulge0  8841  squeeze0  9126  elnn0z  9536  fznlem  10321  frec2uzf1od  10714  seqf1oglem1  10827  facndiv  11047  sumrbdclem  12001  prodrbdclem  12195  alzdvds  12478  fzm1ndvds  12480  fzo0dvdseq  12481  bitsfzolem  12578  bitsfzo  12579  rpdvds  12734  nonsq  12842  prmdiv  12870  odzdvds  12881  pcprendvds  12926  pcprendvds2  12927  pcpremul  12929  pcdvdsb  12956  pcadd2  12977  pockthlem  12992  1arith  13003  4sqlem11  13037  4sqlem17  13043  ennnfonelemim  13108  bldisj  15195  perfect1  15795  lgsdilem2  15838  lgsne0  15840  lgseisenlem1  15872  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  umgrnloop0  16041  bj-nnen2lp  16653  pwtrufal  16702  refeq  16739