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	⊢ (𝜑 → ¬ 𝜒)
mtod.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mtod	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtod

Step	Hyp	Ref	Expression
1		mtod.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mtod.1	. . 3 ⊢ (𝜑 → ¬ 𝜒)
3	2	a1d 22	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 670	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mtoi  674  mtand  675  mtbid  683  mtbird  684  pwntru  4338  po2nr  4456  po3nr  4457  sotricim  4470  elirr  4690  ordn2lp  4694  en2lp  4703  fvdifsuppst  6488  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  nndomo  7170  fnfi  7255  difinfsnlem  7446  nninfwlpoimlemginf  7523  2omotaplemap  7630  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  caucvgprprlemaddq  8082  msqge0  8953  mulge0  8956  squeeze0  9243  elnn0z  9669  fznlem  10463  frec2uzf1od  10865  seqf1oglem1  10978  facndiv  11200  sumrbdclem  12170  prodrbdclem  12364  alzdvds  12647  fzm1ndvds  12649  fzo0dvdseq  12650  bitsfzolem  12747  bitsfzo  12748  rpdvds  12903  nonsq  13013  prmdiv  13043  odzdvds  13054  pcprendvds  13099  pcprendvds2  13100  pcpremul  13102  pcdvdsb  13129  pcadd2  13150  pockthlem  13165  1arith  13176  4sqlem11  13210  4sqlem17  13216  ennnfonelemim  13374  bldisj  15639  chtublem  16307  perfect1  16310  lgsdilem2  16372  lgsne0  16374  lgseisenlem1  16406  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2lem1  16417  umgrnloop0  16575  bj-nnen2lp  17197  pwtrufal  17244  refeq  17291  rirrdisj  17303