Theorem mtod 669

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  670  mtand  671  mtbid  678  mtbird  679  pwntru  4289  po2nr  4406  po3nr  4407  sotricim  4420  elirr  4639  ordn2lp  4643  en2lp  4652  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  nndomo  7050  fnfi  7135  difinfsnlem  7298  nninfwlpoimlemginf  7375  2omotaplemap  7476  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemaddq  7928  msqge0  8796  mulge0  8799  squeeze0  9084  elnn0z  9492  fznlem  10276  frec2uzf1od  10669  seqf1oglem1  10782  facndiv  11002  sumrbdclem  11940  prodrbdclem  12134  alzdvds  12417  fzm1ndvds  12419  fzo0dvdseq  12420  bitsfzolem  12517  bitsfzo  12518  rpdvds  12673  nonsq  12781  prmdiv  12809  odzdvds  12820  pcprendvds  12865  pcprendvds2  12866  pcpremul  12868  pcdvdsb  12895  pcadd2  12916  pockthlem  12931  1arith  12942  4sqlem11  12976  4sqlem17  12982  ennnfonelemim  13047  bldisj  15128  perfect1  15725  lgsdilem2  15768  lgsne0  15770  lgseisenlem1  15802  lgseisenlem2  15803  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2lem1  15813  umgrnloop0  15971  bj-nnen2lp  16570  pwtrufal  16619  refeq  16653