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  4199  po2nr  4309  po3nr  4310  sotricim  4323  elirr  4540  ordn2lp  4544  en2lp  4553  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  nndomo  6863  fnfi  6935  difinfsnlem  7097  nninfwlpoimlemginf  7173  2omotaplemap  7255  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgprlemladdrl  7676  caucvgprprlemaddq  7706  msqge0  8572  mulge0  8575  squeeze0  8860  elnn0z  9265  fznlem  10040  frec2uzf1od  10405  facndiv  10718  sumrbdclem  11384  prodrbdclem  11578  alzdvds  11859  fzm1ndvds  11861  fzo0dvdseq  11862  rpdvds  12098  nonsq  12206  prmdiv  12234  odzdvds  12244  pcprendvds  12289  pcprendvds2  12290  pcpremul  12292  pcdvdsb  12318  pockthlem  12353  1arith  12364  ennnfonelemim  12424  bldisj  13871  lgsdilem2  14407  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  bj-nnen2lp  14676  pwtrufal  14717  refeq  14746