Theorem mtod 658

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 655	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 609  ax-in2 610

This theorem is referenced by:  mtoi  659  mtand  660  mtbid  667  mtbird  668  pwntru  4185  po2nr  4294  po3nr  4295  sotricim  4308  elirr  4525  ordn2lp  4529  en2lp  4538  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  nndomo  6842  fnfi  6914  difinfsnlem  7076  nninfwlpoimlemginf  7152  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgprprlemaddq  7670  msqge0  8535  mulge0  8538  squeeze0  8820  elnn0z  9225  fznlem  9997  frec2uzf1od  10362  facndiv  10673  sumrbdclem  11340  prodrbdclem  11534  alzdvds  11814  fzm1ndvds  11816  fzo0dvdseq  11817  rpdvds  12053  nonsq  12161  prmdiv  12189  odzdvds  12199  pcprendvds  12244  pcprendvds2  12245  pcpremul  12247  pcdvdsb  12273  pockthlem  12308  1arith  12319  ennnfonelemim  12379  bldisj  13195  lgsdilem2  13731  lgsne0  13733  bj-nnen2lp  13989  pwtrufal  14030  refeq  14060