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  4242  po2nr  4355  po3nr  4356  sotricim  4369  elirr  4588  ordn2lp  4592  en2lp  4601  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  nndomo  6960  fnfi  7037  difinfsnlem  7200  nninfwlpoimlemginf  7277  2omotaplemap  7368  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  caucvgprprlemaddq  7820  msqge0  8688  mulge0  8691  squeeze0  8976  elnn0z  9384  fznlem  10162  frec2uzf1od  10549  seqf1oglem1  10662  facndiv  10882  sumrbdclem  11659  prodrbdclem  11853  alzdvds  12136  fzm1ndvds  12138  fzo0dvdseq  12139  bitsfzolem  12236  bitsfzo  12237  rpdvds  12392  nonsq  12500  prmdiv  12528  odzdvds  12539  pcprendvds  12584  pcprendvds2  12585  pcpremul  12587  pcdvdsb  12614  pcadd2  12635  pockthlem  12650  1arith  12661  4sqlem11  12695  4sqlem17  12701  ennnfonelemim  12766  bldisj  14844  perfect1  15441  lgsdilem2  15484  lgsne0  15486  lgseisenlem1  15518  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem1  15529  bj-nnen2lp  15852  pwtrufal  15896  refeq  15929