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  7439  nninfwlpoimlemginf  7516  2omotaplemap  7623  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprprlemaddq  8075  msqge0  8946  mulge0  8949  squeeze0  9236  elnn0z  9661  fznlem  10455  frec2uzf1od  10856  seqf1oglem1  10969  facndiv  11191  sumrbdclem  12160  prodrbdclem  12354  alzdvds  12637  fzm1ndvds  12639  fzo0dvdseq  12640  bitsfzolem  12737  bitsfzo  12738  rpdvds  12893  nonsq  13003  prmdiv  13033  odzdvds  13044  pcprendvds  13089  pcprendvds2  13090  pcpremul  13092  pcdvdsb  13119  pcadd2  13140  pockthlem  13155  1arith  13166  4sqlem11  13200  4sqlem17  13206  ennnfonelemim  13364  bldisj  15551  perfect1  16196  lgsdilem2  16253  lgsne0  16255  lgseisenlem1  16287  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  umgrnloop0  16456  bj-nnen2lp  17078  pwtrufal  17125  refeq  17171