Theorem mtod 653

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  654  mtand  655  mtbid  662  mtbird  663  pwntru  4177  po2nr  4286  po3nr  4287  sotricim  4300  elirr  4517  ordn2lp  4521  en2lp  4530  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  nndomo  6826  fnfi  6898  difinfsnlem  7060  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgprlemladdrl  7615  caucvgprprlemaddq  7645  msqge0  8510  mulge0  8513  squeeze0  8795  elnn0z  9200  fznlem  9972  frec2uzf1od  10337  facndiv  10648  sumrbdclem  11314  prodrbdclem  11508  alzdvds  11788  fzm1ndvds  11790  fzo0dvdseq  11791  rpdvds  12027  nonsq  12135  prmdiv  12163  odzdvds  12173  pcprendvds  12218  pcprendvds2  12219  pcpremul  12221  pcdvdsb  12247  pockthlem  12282  1arith  12293  ennnfonelemim  12353  bldisj  13001  lgsdilem2  13537  lgsne0  13539  bj-nnen2lp  13796  pwtrufal  13837  refeq  13867