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  4201  po2nr  4311  po3nr  4312  sotricim  4325  elirr  4542  ordn2lp  4546  en2lp  4555  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  nndomo  6866  fnfi  6938  difinfsnlem  7100  nninfwlpoimlemginf  7176  2omotaplemap  7258  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  caucvgprprlemaddq  7709  msqge0  8575  mulge0  8578  squeeze0  8863  elnn0z  9268  fznlem  10043  frec2uzf1od  10408  facndiv  10721  sumrbdclem  11387  prodrbdclem  11581  alzdvds  11862  fzm1ndvds  11864  fzo0dvdseq  11865  rpdvds  12101  nonsq  12209  prmdiv  12237  odzdvds  12247  pcprendvds  12292  pcprendvds2  12293  pcpremul  12295  pcdvdsb  12321  pockthlem  12356  1arith  12367  ennnfonelemim  12427  bldisj  13986  lgsdilem2  14522  lgsne0  14524  lgseisenlem1  14535  lgseisenlem2  14536  bj-nnen2lp  14791  pwtrufal  14832  refeq  14861