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  8944  mulge0  8947  squeeze0  9234  elnn0z  9657  fznlem  10445  frec2uzf1od  10843  seqf1oglem1  10956  facndiv  11177  sumrbdclem  12144  prodrbdclem  12338  alzdvds  12621  fzm1ndvds  12623  fzo0dvdseq  12624  bitsfzolem  12721  bitsfzo  12722  rpdvds  12877  nonsq  12985  prmdiv  13013  odzdvds  13024  pcprendvds  13069  pcprendvds2  13070  pcpremul  13072  pcdvdsb  13099  pcadd2  13120  pockthlem  13135  1arith  13146  4sqlem11  13180  4sqlem17  13186  ennnfonelemim  13315  bldisj  15502  perfect1  16112  lgsdilem2  16155  lgsne0  16157  lgseisenlem1  16189  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  umgrnloop0  16358  bj-nnen2lp  16980  pwtrufal  17027  refeq  17073