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  678  mtbird  679  pwntru  4289  po2nr  4406  po3nr  4407  sotricim  4420  elirr  4639  ordn2lp  4643  en2lp  4652  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  nndomo  7050  fnfi  7135  difinfsnlem  7298  nninfwlpoimlemginf  7375  2omotaplemap  7476  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemaddq  7928  msqge0  8796  mulge0  8799  squeeze0  9084  elnn0z  9492  fznlem  10276  frec2uzf1od  10668  seqf1oglem1  10781  facndiv  11001  sumrbdclem  11939  prodrbdclem  12133  alzdvds  12416  fzm1ndvds  12418  fzo0dvdseq  12419  bitsfzolem  12516  bitsfzo  12517  rpdvds  12672  nonsq  12780  prmdiv  12808  odzdvds  12819  pcprendvds  12864  pcprendvds2  12865  pcpremul  12867  pcdvdsb  12894  pcadd2  12915  pockthlem  12930  1arith  12941  4sqlem11  12975  4sqlem17  12981  ennnfonelemim  13046  bldisj  15127  perfect1  15724  lgsdilem2  15767  lgsne0  15769  lgseisenlem1  15801  lgseisenlem2  15802  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  lgsquad2lem1  15812  umgrnloop0  15970  bj-nnen2lp  16552  pwtrufal  16601  refeq  16635