Theorem mtod 669

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 666	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 619  ax-in2 620

This theorem is referenced by:  mtoi  670  mtand  671  mtbid  679  mtbird  680  pwntru  4312  po2nr  4430  po3nr  4431  sotricim  4444  elirr  4663  ordn2lp  4667  en2lp  4676  fvdifsuppst  6444  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  nndomo  7118  fnfi  7203  difinfsnlem  7390  nninfwlpoimlemginf  7467  2omotaplemap  7571  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  caucvgprprlemaddq  8023  msqge0  8890  mulge0  8893  squeeze0  9178  elnn0z  9590  fznlem  10375  frec2uzf1od  10768  seqf1oglem1  10881  facndiv  11101  sumrbdclem  12063  prodrbdclem  12257  alzdvds  12540  fzm1ndvds  12542  fzo0dvdseq  12543  bitsfzolem  12640  bitsfzo  12641  rpdvds  12796  nonsq  12904  prmdiv  12932  odzdvds  12943  pcprendvds  12988  pcprendvds2  12989  pcpremul  12991  pcdvdsb  13018  pcadd2  13039  pockthlem  13054  1arith  13065  4sqlem11  13099  4sqlem17  13105  ennnfonelemim  13175  bldisj  15266  perfect1  15866  lgsdilem2  15909  lgsne0  15911  lgseisenlem1  15943  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  umgrnloop0  16112  bj-nnen2lp  16724  pwtrufal  16771  refeq  16808