Theorem mtod 663

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  664  mtand  665  mtbid  672  mtbird  673  pwntru  4200  po2nr  4310  po3nr  4311  sotricim  4324  elirr  4541  ordn2lp  4545  en2lp  4554  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  nndomo  6864  fnfi  6936  difinfsnlem  7098  nninfwlpoimlemginf  7174  2omotaplemap  7256  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemladdrl  7677  caucvgprprlemaddq  7707  msqge0  8573  mulge0  8576  squeeze0  8861  elnn0z  9266  fznlem  10041  frec2uzf1od  10406  facndiv  10719  sumrbdclem  11385  prodrbdclem  11579  alzdvds  11860  fzm1ndvds  11862  fzo0dvdseq  11863  rpdvds  12099  nonsq  12207  prmdiv  12235  odzdvds  12245  pcprendvds  12290  pcprendvds2  12291  pcpremul  12293  pcdvdsb  12319  pockthlem  12354  1arith  12365  ennnfonelemim  12425  bldisj  13904  lgsdilem2  14440  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  bj-nnen2lp  14709  pwtrufal  14750  refeq  14779