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  4282  po2nr  4399  po3nr  4400  sotricim  4413  elirr  4632  ordn2lp  4636  en2lp  4645  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  nndomo  7021  fnfi  7099  difinfsnlem  7262  nninfwlpoimlemginf  7339  2omotaplemap  7439  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  caucvgprprlemaddq  7891  msqge0  8759  mulge0  8762  squeeze0  9047  elnn0z  9455  fznlem  10233  frec2uzf1od  10623  seqf1oglem1  10736  facndiv  10956  sumrbdclem  11883  prodrbdclem  12077  alzdvds  12360  fzm1ndvds  12362  fzo0dvdseq  12363  bitsfzolem  12460  bitsfzo  12461  rpdvds  12616  nonsq  12724  prmdiv  12752  odzdvds  12763  pcprendvds  12808  pcprendvds2  12809  pcpremul  12811  pcdvdsb  12838  pcadd2  12859  pockthlem  12874  1arith  12885  4sqlem11  12919  4sqlem17  12925  ennnfonelemim  12990  bldisj  15069  perfect1  15666  lgsdilem2  15709  lgsne0  15711  lgseisenlem1  15743  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  umgrnloop0  15911  bj-nnen2lp  16275  pwtrufal  16322  refeq  16355