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  4336  po2nr  4454  po3nr  4455  sotricim  4468  elirr  4688  ordn2lp  4692  en2lp  4701  fvdifsuppst  6484  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  nndomo  7165  fnfi  7250  difinfsnlem  7439  nninfwlpoimlemginf  7516  2omotaplemap  7623  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprprlemaddq  8075  msqge0  8945  mulge0  8948  squeeze0  9235  elnn0z  9659  fznlem  10447  frec2uzf1od  10845  seqf1oglem1  10958  facndiv  11179  sumrbdclem  12146  prodrbdclem  12340  alzdvds  12623  fzm1ndvds  12625  fzo0dvdseq  12626  bitsfzolem  12723  bitsfzo  12724  rpdvds  12879  nonsq  12987  prmdiv  13015  odzdvds  13026  pcprendvds  13071  pcprendvds2  13072  pcpremul  13074  pcdvdsb  13101  pcadd2  13122  pockthlem  13137  1arith  13148  4sqlem11  13182  4sqlem17  13188  ennnfonelemim  13317  bldisj  15504  perfect1  16118  lgsdilem2  16167  lgsne0  16169  lgseisenlem1  16201  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2lem1  16212  umgrnloop0  16370  bj-nnen2lp  16992  pwtrufal  17039  refeq  17085