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  678  mtbird  679  pwntru  4289  po2nr  4406  po3nr  4407  sotricim  4420  elirr  4639  ordn2lp  4643  en2lp  4652  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  nndomo  7050  fnfi  7135  difinfsnlem  7298  nninfwlpoimlemginf  7375  2omotaplemap  7476  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemaddq  7928  msqge0  8796  mulge0  8799  squeeze0  9084  elnn0z  9492  fznlem  10276  frec2uzf1od  10669  seqf1oglem1  10782  facndiv  11002  sumrbdclem  11956  prodrbdclem  12150  alzdvds  12433  fzm1ndvds  12435  fzo0dvdseq  12436  bitsfzolem  12533  bitsfzo  12534  rpdvds  12689  nonsq  12797  prmdiv  12825  odzdvds  12836  pcprendvds  12881  pcprendvds2  12882  pcpremul  12884  pcdvdsb  12911  pcadd2  12932  pockthlem  12947  1arith  12958  4sqlem11  12992  4sqlem17  12998  ennnfonelemim  13063  bldisj  15144  perfect1  15741  lgsdilem2  15784  lgsne0  15786  lgseisenlem1  15818  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  umgrnloop0  15987  bj-nnen2lp  16600  pwtrufal  16649  refeq  16683