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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  674  mtand  675  mtbid  683  mtbird  684  pwntru  4334  po2nr  4452  po3nr  4453  sotricim  4466  elirr  4686  ordn2lp  4690  en2lp  4699  fvdifsuppst  6478  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  nndomo  7159  fnfi  7244  difinfsnlem  7433  nninfwlpoimlemginf  7510  2omotaplemap  7617  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  caucvgprprlemaddq  8069  msqge0  8938  mulge0  8941  squeeze0  9228  elnn0z  9640  fznlem  10428  frec2uzf1od  10826  seqf1oglem1  10939  facndiv  11160  sumrbdclem  12127  prodrbdclem  12321  alzdvds  12604  fzm1ndvds  12606  fzo0dvdseq  12607  bitsfzolem  12704  bitsfzo  12705  rpdvds  12860  nonsq  12968  prmdiv  12996  odzdvds  13007  pcprendvds  13052  pcprendvds2  13053  pcpremul  13055  pcdvdsb  13082  pcadd2  13103  pockthlem  13118  1arith  13129  4sqlem11  13163  4sqlem17  13169  ennnfonelemim  13298  bldisj  15485  perfect1  16095  lgsdilem2  16138  lgsne0  16140  lgseisenlem1  16172  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem1  16183  umgrnloop0  16341  bj-nnen2lp  16963  pwtrufal  17010  refeq  17047