Theorem mtod 673

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 670	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 623  ax-in2 624

This theorem is referenced by:  mtoi  674  mtand  675  mtbid  683  mtbird  684  pwntru  4331  po2nr  4449  po3nr  4450  sotricim  4463  elirr  4683  ordn2lp  4687  en2lp  4696  fvdifsuppst  6474  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  nndomo  7155  fnfi  7240  difinfsnlem  7429  nninfwlpoimlemginf  7506  2omotaplemap  7613  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  caucvgprprlemaddq  8065  msqge0  8934  mulge0  8937  squeeze0  9224  elnn0z  9636  fznlem  10424  frec2uzf1od  10821  seqf1oglem1  10934  facndiv  11155  sumrbdclem  12122  prodrbdclem  12316  alzdvds  12599  fzm1ndvds  12601  fzo0dvdseq  12602  bitsfzolem  12699  bitsfzo  12700  rpdvds  12855  nonsq  12963  prmdiv  12991  odzdvds  13002  pcprendvds  13047  pcprendvds2  13048  pcpremul  13050  pcdvdsb  13077  pcadd2  13098  pockthlem  13113  1arith  13124  4sqlem11  13158  4sqlem17  13164  ennnfonelemim  13293  bldisj  15425  perfect1  16026  lgsdilem2  16069  lgsne0  16071  lgseisenlem1  16103  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  umgrnloop0  16272  bj-nnen2lp  16894  pwtrufal  16941  refeq  16978