Theorem mtod 664

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  665  mtand  666  mtbid  673  mtbird  674  pwntru  4233  po2nr  4345  po3nr  4346  sotricim  4359  elirr  4578  ordn2lp  4582  en2lp  4591  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  nndomo  6934  fnfi  7011  difinfsnlem  7174  nninfwlpoimlemginf  7251  2omotaplemap  7342  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  caucvgprprlemaddq  7794  msqge0  8662  mulge0  8665  squeeze0  8950  elnn0z  9358  fznlem  10135  frec2uzf1od  10517  seqf1oglem1  10630  facndiv  10850  sumrbdclem  11561  prodrbdclem  11755  alzdvds  12038  fzm1ndvds  12040  fzo0dvdseq  12041  bitsfzolem  12138  bitsfzo  12139  rpdvds  12294  nonsq  12402  prmdiv  12430  odzdvds  12441  pcprendvds  12486  pcprendvds2  12487  pcpremul  12489  pcdvdsb  12516  pcadd2  12537  pockthlem  12552  1arith  12563  4sqlem11  12597  4sqlem17  12603  ennnfonelemim  12668  bldisj  14745  perfect1  15342  lgsdilem2  15385  lgsne0  15387  lgseisenlem1  15419  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  bj-nnen2lp  15708  pwtrufal  15752  refeq  15785