Theorem mtod 665

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 662	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 615  ax-in2 616

This theorem is referenced by:  mtoi  666  mtand  667  mtbid  674  mtbird  675  pwntru  4247  po2nr  4360  po3nr  4361  sotricim  4374  elirr  4593  ordn2lp  4597  en2lp  4606  tfr1onlemsucaccv  6434  tfrcllemsucaccv  6447  nndomo  6968  fnfi  7045  difinfsnlem  7208  nninfwlpoimlemginf  7285  2omotaplemap  7376  cauappcvgprlemladdru  7776  cauappcvgprlemladdrl  7777  caucvgprlemladdrl  7798  caucvgprprlemaddq  7828  msqge0  8696  mulge0  8699  squeeze0  8984  elnn0z  9392  fznlem  10170  frec2uzf1od  10558  seqf1oglem1  10671  facndiv  10891  sumrbdclem  11732  prodrbdclem  11926  alzdvds  12209  fzm1ndvds  12211  fzo0dvdseq  12212  bitsfzolem  12309  bitsfzo  12310  rpdvds  12465  nonsq  12573  prmdiv  12601  odzdvds  12612  pcprendvds  12657  pcprendvds2  12658  pcpremul  12660  pcdvdsb  12687  pcadd2  12708  pockthlem  12723  1arith  12734  4sqlem11  12768  4sqlem17  12774  ennnfonelemim  12839  bldisj  14917  perfect1  15514  lgsdilem2  15557  lgsne0  15559  lgseisenlem1  15591  lgseisenlem2  15592  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad2lem1  15602  bj-nnen2lp  15964  pwtrufal  16008  refeq  16041