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

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  679  mtbird  680  pwntru  4317  po2nr  4435  po3nr  4436  sotricim  4449  elirr  4668  ordn2lp  4672  en2lp  4681  fvdifsuppst  6457  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  nndomo  7131  fnfi  7216  difinfsnlem  7403  nninfwlpoimlemginf  7480  2omotaplemap  7587  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemaddq  8039  msqge0  8908  mulge0  8911  squeeze0  9198  elnn0z  9610  fznlem  10398  frec2uzf1od  10795  seqf1oglem1  10908  facndiv  11129  sumrbdclem  12091  prodrbdclem  12285  alzdvds  12568  fzm1ndvds  12570  fzo0dvdseq  12571  bitsfzolem  12668  bitsfzo  12669  rpdvds  12824  nonsq  12932  prmdiv  12960  odzdvds  12971  pcprendvds  13016  pcprendvds2  13017  pcpremul  13019  pcdvdsb  13046  pcadd2  13067  pockthlem  13082  1arith  13093  4sqlem11  13127  4sqlem17  13133  ennnfonelemim  13262  bldisj  15395  perfect1  15995  lgsdilem2  16038  lgsne0  16040  lgseisenlem1  16072  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2lem1  16083  umgrnloop0  16241  bj-nnen2lp  16863  pwtrufal  16910  refeq  16947