Theorem mtod 673

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 670	1 |- ( ph -> -. ps )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mtoi  674  mtand  675  mtbid  683  mtbird  684  pwntru  4336  po2nr  4454  po3nr  4455  sotricim  4468  elirr  4688  ordn2lp  4692  en2lp  4701  fvdifsuppst  6484  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  nndomo  7165  fnfi  7250  difinfsnlem  7440  nninfwlpoimlemginf  7517  2omotaplemap  7624  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprprlemaddq  8076  msqge0  8947  mulge0  8950  squeeze0  9237  elnn0z  9662  fznlem  10456  frec2uzf1od  10858  seqf1oglem1  10971  facndiv  11193  sumrbdclem  12163  prodrbdclem  12357  alzdvds  12640  fzm1ndvds  12642  fzo0dvdseq  12643  bitsfzolem  12740  bitsfzo  12741  rpdvds  12896  nonsq  13006  prmdiv  13036  odzdvds  13047  pcprendvds  13092  pcprendvds2  13093  pcpremul  13095  pcdvdsb  13122  pcadd2  13143  pockthlem  13158  1arith  13169  4sqlem11  13203  4sqlem17  13209  ennnfonelemim  13367  bldisj  15593  chtublem  16256  perfect1  16259  lgsdilem2  16321  lgsne0  16323  lgseisenlem1  16355  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem1  16366  umgrnloop0  16524  bj-nnen2lp  17146  pwtrufal  17193  refeq  17239  rirrdisj  17251