Theorem mtod 664

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 661	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 615  ax-in2 616

This theorem is referenced by:  mtoi  665  mtand  666  mtbid  673  mtbird  674  pwntru  4229  po2nr  4341  po3nr  4342  sotricim  4355  elirr  4574  ordn2lp  4578  en2lp  4587  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  nndomo  6922  fnfi  6997  difinfsnlem  7160  nninfwlpoimlemginf  7237  2omotaplemap  7319  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  caucvgprprlemaddq  7770  msqge0  8637  mulge0  8640  squeeze0  8925  elnn0z  9333  fznlem  10110  frec2uzf1od  10480  seqf1oglem1  10593  facndiv  10813  sumrbdclem  11523  prodrbdclem  11717  alzdvds  11999  fzm1ndvds  12001  fzo0dvdseq  12002  rpdvds  12240  nonsq  12348  prmdiv  12376  odzdvds  12386  pcprendvds  12431  pcprendvds2  12432  pcpremul  12434  pcdvdsb  12461  pcadd2  12482  pockthlem  12497  1arith  12508  4sqlem11  12542  4sqlem17  12548  ennnfonelemim  12584  bldisj  14580  lgsdilem2  15193  lgsne0  15195  lgseisenlem1  15227  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  bj-nnen2lp  15516  pwtrufal  15558  refeq  15588