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  4338  po2nr  4456  po3nr  4457  sotricim  4470  elirr  4690  ordn2lp  4694  en2lp  4703  fvdifsuppst  6488  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  nndomo  7169  fnfi  7254  difinfsnlem  7445  nninfwlpoimlemginf  7522  2omotaplemap  7629  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemaddq  8081  msqge0  8952  mulge0  8955  squeeze0  9242  elnn0z  9668  fznlem  10462  frec2uzf1od  10864  seqf1oglem1  10977  facndiv  11199  sumrbdclem  12169  prodrbdclem  12363  alzdvds  12646  fzm1ndvds  12648  fzo0dvdseq  12649  bitsfzolem  12746  bitsfzo  12747  rpdvds  12902  nonsq  13012  prmdiv  13042  odzdvds  13053  pcprendvds  13098  pcprendvds2  13099  pcpremul  13101  pcdvdsb  13128  pcadd2  13149  pockthlem  13164  1arith  13175  4sqlem11  13209  4sqlem17  13215  ennnfonelemim  13373  bldisj  15627  chtublem  16295  perfect1  16298  lgsdilem2  16360  lgsne0  16362  lgseisenlem1  16394  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem1  16405  umgrnloop0  16563  bj-nnen2lp  17185  pwtrufal  17232  refeq  17279  rirrdisj  17291