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  7440  nninfwlpoimlemginf  7517  2omotaplemap  7624  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprprlemaddq  8076  msqge0  8947  mulge0  8950  squeeze0  9237  elnn0z  9662  fznlem  10456  frec2uzf1od  10857  seqf1oglem1  10970  facndiv  11192  sumrbdclem  12162  prodrbdclem  12356  alzdvds  12639  fzm1ndvds  12641  fzo0dvdseq  12642  bitsfzolem  12739  bitsfzo  12740  rpdvds  12895  nonsq  13005  prmdiv  13035  odzdvds  13046  pcprendvds  13091  pcprendvds2  13092  pcpremul  13094  pcdvdsb  13121  pcadd2  13142  pockthlem  13157  1arith  13168  4sqlem11  13202  4sqlem17  13208  ennnfonelemim  13366  bldisj  15554  chtublem  16217  perfect1  16220  lgsdilem2  16277  lgsne0  16279  lgseisenlem1  16311  lgseisenlem2  16312  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad2lem1  16322  umgrnloop0  16480  bj-nnen2lp  17102  pwtrufal  17149  refeq  17195