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  6617  tfrcllemsucaccv  6630  nndomo  7171  fnfi  7256  difinfsnlem  7445  nninfwlpoimlemginf  7522  2omotaplemap  7629  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemaddq  8081  msqge0  8952  mulge0  8955  squeeze0  9242  elnn0z  9666  fznlem  10461  frec2uzf1od  10863  seqf1oglem1  10976  facndiv  11198  sumrbdclem  12168  prodrbdclem  12362  alzdvds  12645  fzm1ndvds  12647  fzo0dvdseq  12648  bitsfzolem  12745  bitsfzo  12746  rpdvds  12901  nonsq  13011  prmdiv  13041  odzdvds  13052  pcprendvds  13097  pcprendvds2  13098  pcpremul  13100  pcdvdsb  13127  pcadd2  13148  pockthlem  13163  1arith  13174  4sqlem11  13208  4sqlem17  13214  ennnfonelemim  13372  bldisj  15644  chtublem  16312  perfect1  16315  lgsdilem2  16377  lgsne0  16379  lgseisenlem1  16411  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem1  16422  umgrnloop0  16580  bj-nnen2lp  17202  pwtrufal  17249  refeq  17296  rirrdisj  17308