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  4232  po2nr  4344  po3nr  4345  sotricim  4358  elirr  4577  ordn2lp  4581  en2lp  4590  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  nndomo  6925  fnfi  7002  difinfsnlem  7165  nninfwlpoimlemginf  7242  2omotaplemap  7324  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  caucvgprprlemaddq  7775  msqge0  8643  mulge0  8646  squeeze0  8931  elnn0z  9339  fznlem  10116  frec2uzf1od  10498  seqf1oglem1  10611  facndiv  10831  sumrbdclem  11542  prodrbdclem  11736  alzdvds  12019  fzm1ndvds  12021  fzo0dvdseq  12022  bitsfzolem  12118  bitsfzo  12119  rpdvds  12267  nonsq  12375  prmdiv  12403  odzdvds  12414  pcprendvds  12459  pcprendvds2  12460  pcpremul  12462  pcdvdsb  12489  pcadd2  12510  pockthlem  12525  1arith  12536  4sqlem11  12570  4sqlem17  12576  ennnfonelemim  12641  bldisj  14637  perfect1  15234  lgsdilem2  15277  lgsne0  15279  lgseisenlem1  15311  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  bj-nnen2lp  15600  pwtrufal  15642  refeq  15672