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  4314  po2nr  4432  po3nr  4433  sotricim  4446  elirr  4665  ordn2lp  4669  en2lp  4678  fvdifsuppst  6446  tfr1onlemsucaccv  6574  tfrcllemsucaccv  6587  nndomo  7120  fnfi  7205  difinfsnlem  7392  nninfwlpoimlemginf  7469  2omotaplemap  7573  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgprlemladdrl  7995  caucvgprprlemaddq  8025  msqge0  8892  mulge0  8895  squeeze0  9180  elnn0z  9592  fznlem  10378  frec2uzf1od  10772  seqf1oglem1  10885  facndiv  11105  sumrbdclem  12067  prodrbdclem  12261  alzdvds  12544  fzm1ndvds  12546  fzo0dvdseq  12547  bitsfzolem  12644  bitsfzo  12645  rpdvds  12800  nonsq  12908  prmdiv  12936  odzdvds  12947  pcprendvds  12992  pcprendvds2  12993  pcpremul  12995  pcdvdsb  13022  pcadd2  13043  pockthlem  13058  1arith  13069  4sqlem11  13103  4sqlem17  13109  ennnfonelemim  13192  bldisj  15283  perfect1  15883  lgsdilem2  15926  lgsne0  15928  lgseisenlem1  15960  lgseisenlem2  15961  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  lgsquad2lem1  15971  umgrnloop0  16129  bj-nnen2lp  16741  pwtrufal  16788  refeq  16825