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  678  mtbird  679  pwntru  4289  po2nr  4406  po3nr  4407  sotricim  4420  elirr  4639  ordn2lp  4643  en2lp  4652  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  nndomo  7049  fnfi  7134  difinfsnlem  7297  nninfwlpoimlemginf  7374  2omotaplemap  7475  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  caucvgprprlemaddq  7927  msqge0  8795  mulge0  8798  squeeze0  9083  elnn0z  9491  fznlem  10275  frec2uzf1od  10667  seqf1oglem1  10780  facndiv  11000  sumrbdclem  11937  prodrbdclem  12131  alzdvds  12414  fzm1ndvds  12416  fzo0dvdseq  12417  bitsfzolem  12514  bitsfzo  12515  rpdvds  12670  nonsq  12778  prmdiv  12806  odzdvds  12817  pcprendvds  12862  pcprendvds2  12863  pcpremul  12865  pcdvdsb  12892  pcadd2  12913  pockthlem  12928  1arith  12939  4sqlem11  12973  4sqlem17  12979  ennnfonelemim  13044  bldisj  15124  perfect1  15721  lgsdilem2  15764  lgsne0  15766  lgseisenlem1  15798  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  umgrnloop0  15967  bj-nnen2lp  16549  pwtrufal  16598  refeq  16632