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  4228  po2nr  4340  po3nr  4341  sotricim  4354  elirr  4573  ordn2lp  4577  en2lp  4586  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  nndomo  6920  fnfi  6995  difinfsnlem  7158  nninfwlpoimlemginf  7235  2omotaplemap  7317  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  caucvgprprlemaddq  7768  msqge0  8635  mulge0  8638  squeeze0  8923  elnn0z  9330  fznlem  10107  frec2uzf1od  10477  seqf1oglem1  10590  facndiv  10810  sumrbdclem  11520  prodrbdclem  11714  alzdvds  11996  fzm1ndvds  11998  fzo0dvdseq  11999  rpdvds  12237  nonsq  12345  prmdiv  12373  odzdvds  12383  pcprendvds  12428  pcprendvds2  12429  pcpremul  12431  pcdvdsb  12458  pcadd2  12479  pockthlem  12494  1arith  12505  4sqlem11  12539  4sqlem17  12545  ennnfonelemim  12581  bldisj  14569  lgsdilem2  15152  lgsne0  15154  lgseisenlem1  15186  lgseisenlem2  15187  lgsquadlem1  15191  bj-nnen2lp  15446  pwtrufal  15488  refeq  15518