Theorem mtod 652

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  653  mtand  654  mtbid  661  mtbird  662  pwntru  4122  po2nr  4231  po3nr  4232  sotricim  4245  elirr  4456  ordn2lp  4460  en2lp  4469  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  nndomo  6758  fnfi  6825  difinfsnlem  6984  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  caucvgprprlemaddq  7516  msqge0  8378  mulge0  8381  squeeze0  8662  elnn0z  9067  fznlem  9821  frec2uzf1od  10179  facndiv  10485  sumrbdclem  11146  prodrbdclem  11340  alzdvds  11552  fzm1ndvds  11554  fzo0dvdseq  11555  rpdvds  11780  nonsq  11885  ennnfonelemim  11937  bldisj  12570  bj-nnen2lp  13152  pwtrufal  13192  refeq  13223