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  4314  po2nr  4432  po3nr  4433  sotricim  4446  elirr  4665  ordn2lp  4669  en2lp  4678  fvdifsuppst  6446  tfr1onlemsucaccv  6574  tfrcllemsucaccv  6587  nndomo  7120  fnfi  7205  difinfsnlem  7392  nninfwlpoimlemginf  7469  2omotaplemap  7576  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  caucvgprlemladdrl  7998  caucvgprprlemaddq  8028  msqge0  8895  mulge0  8898  squeeze0  9183  elnn0z  9595  fznlem  10381  frec2uzf1od  10775  seqf1oglem1  10888  facndiv  11109  sumrbdclem  12071  prodrbdclem  12265  alzdvds  12548  fzm1ndvds  12550  fzo0dvdseq  12551  bitsfzolem  12648  bitsfzo  12649  rpdvds  12804  nonsq  12912  prmdiv  12940  odzdvds  12951  pcprendvds  12996  pcprendvds2  12997  pcpremul  12999  pcdvdsb  13026  pcadd2  13047  pockthlem  13062  1arith  13073  4sqlem11  13107  4sqlem17  13113  ennnfonelemim  13196  bldisj  15315  perfect1  15915  lgsdilem2  15958  lgsne0  15960  lgseisenlem1  15992  lgseisenlem2  15993  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2lem1  16003  umgrnloop0  16161  bj-nnen2lp  16773  pwtrufal  16820  refeq  16857