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  4233  po2nr  4345  po3nr  4346  sotricim  4359  elirr  4578  ordn2lp  4582  en2lp  4591  tfr1onlemsucaccv  6400  tfrcllemsucaccv  6413  nndomo  6926  fnfi  7003  difinfsnlem  7166  nninfwlpoimlemginf  7243  2omotaplemap  7326  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  caucvgprlemladdrl  7747  caucvgprprlemaddq  7777  msqge0  8645  mulge0  8648  squeeze0  8933  elnn0z  9341  fznlem  10118  frec2uzf1od  10500  seqf1oglem1  10613  facndiv  10833  sumrbdclem  11544  prodrbdclem  11738  alzdvds  12021  fzm1ndvds  12023  fzo0dvdseq  12024  bitsfzolem  12121  bitsfzo  12122  rpdvds  12277  nonsq  12385  prmdiv  12413  odzdvds  12424  pcprendvds  12469  pcprendvds2  12470  pcpremul  12472  pcdvdsb  12499  pcadd2  12520  pockthlem  12535  1arith  12546  4sqlem11  12580  4sqlem17  12586  ennnfonelemim  12651  bldisj  14647  perfect1  15244  lgsdilem2  15287  lgsne0  15289  lgseisenlem1  15321  lgseisenlem2  15322  lgsquadlem1  15328  lgsquadlem2  15329  lgsquadlem3  15330  lgsquad2lem1  15332  bj-nnen2lp  15610  pwtrufal  15652  refeq  15682