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  6408  tfrcllemsucaccv  6421  nndomo  6934  fnfi  7011  difinfsnlem  7174  nninfwlpoimlemginf  7251  2omotaplemap  7340  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  caucvgprprlemaddq  7792  msqge0  8660  mulge0  8663  squeeze0  8948  elnn0z  9356  fznlem  10133  frec2uzf1od  10515  seqf1oglem1  10628  facndiv  10848  sumrbdclem  11559  prodrbdclem  11753  alzdvds  12036  fzm1ndvds  12038  fzo0dvdseq  12039  bitsfzolem  12136  bitsfzo  12137  rpdvds  12292  nonsq  12400  prmdiv  12428  odzdvds  12439  pcprendvds  12484  pcprendvds2  12485  pcpremul  12487  pcdvdsb  12514  pcadd2  12535  pockthlem  12550  1arith  12561  4sqlem11  12595  4sqlem17  12601  ennnfonelemim  12666  bldisj  14721  perfect1  15318  lgsdilem2  15361  lgsne0  15363  lgseisenlem1  15395  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  bj-nnen2lp  15684  pwtrufal  15728  refeq  15759