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  4283  po2nr  4400  po3nr  4401  sotricim  4414  elirr  4633  ordn2lp  4637  en2lp  4646  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  nndomo  7033  fnfi  7114  difinfsnlem  7277  nninfwlpoimlemginf  7354  2omotaplemap  7454  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgprprlemaddq  7906  msqge0  8774  mulge0  8777  squeeze0  9062  elnn0z  9470  fznlem  10249  frec2uzf1od  10640  seqf1oglem1  10753  facndiv  10973  sumrbdclem  11903  prodrbdclem  12097  alzdvds  12380  fzm1ndvds  12382  fzo0dvdseq  12383  bitsfzolem  12480  bitsfzo  12481  rpdvds  12636  nonsq  12744  prmdiv  12772  odzdvds  12783  pcprendvds  12828  pcprendvds2  12829  pcpremul  12831  pcdvdsb  12858  pcadd2  12879  pockthlem  12894  1arith  12905  4sqlem11  12939  4sqlem17  12945  ennnfonelemim  13010  bldisj  15090  perfect1  15687  lgsdilem2  15730  lgsne0  15732  lgseisenlem1  15764  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  umgrnloop0  15932  bj-nnen2lp  16372  pwtrufal  16422  refeq  16456