Theorem mtod 669

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 619  ax-in2 620

This theorem is referenced by:  mtoi  670  mtand  671  mtbid  679  mtbird  680  pwntru  4317  po2nr  4435  po3nr  4436  sotricim  4449  elirr  4668  ordn2lp  4672  en2lp  4681  fvdifsuppst  6457  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  nndomo  7131  fnfi  7216  difinfsnlem  7403  nninfwlpoimlemginf  7480  2omotaplemap  7587  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemaddq  8039  msqge0  8907  mulge0  8910  squeeze0  9195  elnn0z  9607  fznlem  10395  frec2uzf1od  10792  seqf1oglem1  10905  facndiv  11126  sumrbdclem  12088  prodrbdclem  12282  alzdvds  12565  fzm1ndvds  12567  fzo0dvdseq  12568  bitsfzolem  12665  bitsfzo  12666  rpdvds  12821  nonsq  12929  prmdiv  12957  odzdvds  12968  pcprendvds  13013  pcprendvds2  13014  pcpremul  13016  pcdvdsb  13043  pcadd2  13064  pockthlem  13079  1arith  13090  4sqlem11  13124  4sqlem17  13130  ennnfonelemim  13259  bldisj  15392  perfect1  15992  lgsdilem2  16035  lgsne0  16037  lgseisenlem1  16069  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  umgrnloop0  16238  bj-nnen2lp  16850  pwtrufal  16897  refeq  16934