Theorem mtod 663

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 660	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 614  ax-in2 615

This theorem is referenced by:  mtoi  664  mtand  665  mtbid  672  mtbird  673  pwntru  4201  po2nr  4311  po3nr  4312  sotricim  4325  elirr  4542  ordn2lp  4546  en2lp  4555  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  nndomo  6866  fnfi  6938  difinfsnlem  7100  nninfwlpoimlemginf  7176  2omotaplemap  7258  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  caucvgprprlemaddq  7709  msqge0  8575  mulge0  8578  squeeze0  8863  elnn0z  9268  fznlem  10043  frec2uzf1od  10408  facndiv  10721  sumrbdclem  11387  prodrbdclem  11581  alzdvds  11862  fzm1ndvds  11864  fzo0dvdseq  11865  rpdvds  12101  nonsq  12209  prmdiv  12237  odzdvds  12247  pcprendvds  12292  pcprendvds2  12293  pcpremul  12295  pcdvdsb  12321  pockthlem  12356  1arith  12367  ennnfonelemim  12427  bldisj  13940  lgsdilem2  14476  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  bj-nnen2lp  14745  pwtrufal  14786  refeq  14815