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  4243  po2nr  4356  po3nr  4357  sotricim  4370  elirr  4589  ordn2lp  4593  en2lp  4602  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  nndomo  6961  fnfi  7038  difinfsnlem  7201  nninfwlpoimlemginf  7278  2omotaplemap  7369  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  caucvgprprlemaddq  7821  msqge0  8689  mulge0  8692  squeeze0  8977  elnn0z  9385  fznlem  10163  frec2uzf1od  10551  seqf1oglem1  10664  facndiv  10884  sumrbdclem  11688  prodrbdclem  11882  alzdvds  12165  fzm1ndvds  12167  fzo0dvdseq  12168  bitsfzolem  12265  bitsfzo  12266  rpdvds  12421  nonsq  12529  prmdiv  12557  odzdvds  12568  pcprendvds  12613  pcprendvds2  12614  pcpremul  12616  pcdvdsb  12643  pcadd2  12664  pockthlem  12679  1arith  12690  4sqlem11  12724  4sqlem17  12730  ennnfonelemim  12795  bldisj  14873  perfect1  15470  lgsdilem2  15513  lgsne0  15515  lgseisenlem1  15547  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  bj-nnen2lp  15890  pwtrufal  15934  refeq  15967