Theorem mtod 667

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 664	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 617  ax-in2 618

This theorem is referenced by:  mtoi  668  mtand  669  mtbid  676  mtbird  677  pwntru  4287  po2nr  4404  po3nr  4405  sotricim  4418  elirr  4637  ordn2lp  4641  en2lp  4650  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  nndomo  7045  fnfi  7126  difinfsnlem  7289  nninfwlpoimlemginf  7366  2omotaplemap  7466  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  caucvgprprlemaddq  7918  msqge0  8786  mulge0  8789  squeeze0  9074  elnn0z  9482  fznlem  10266  frec2uzf1od  10658  seqf1oglem1  10771  facndiv  10991  sumrbdclem  11928  prodrbdclem  12122  alzdvds  12405  fzm1ndvds  12407  fzo0dvdseq  12408  bitsfzolem  12505  bitsfzo  12506  rpdvds  12661  nonsq  12769  prmdiv  12797  odzdvds  12808  pcprendvds  12853  pcprendvds2  12854  pcpremul  12856  pcdvdsb  12883  pcadd2  12904  pockthlem  12919  1arith  12930  4sqlem11  12964  4sqlem17  12970  ennnfonelemim  13035  bldisj  15115  perfect1  15712  lgsdilem2  15755  lgsne0  15757  lgseisenlem1  15789  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  umgrnloop0  15958  bj-nnen2lp  16485  pwtrufal  16534  refeq  16568