Theorem mtod 667

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtoi  668  mtand  669  mtbid  676  mtbird  677  pwntru  4287  po2nr  4404  po3nr  4405  sotricim  4418  elirr  4637  ordn2lp  4641  en2lp  4650  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  nndomo  7045  fnfi  7129  difinfsnlem  7292  nninfwlpoimlemginf  7369  2omotaplemap  7469  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemladdrl  7891  caucvgprprlemaddq  7921  msqge0  8789  mulge0  8792  squeeze0  9077  elnn0z  9485  fznlem  10269  frec2uzf1od  10661  seqf1oglem1  10774  facndiv  10994  sumrbdclem  11931  prodrbdclem  12125  alzdvds  12408  fzm1ndvds  12410  fzo0dvdseq  12411  bitsfzolem  12508  bitsfzo  12509  rpdvds  12664  nonsq  12772  prmdiv  12800  odzdvds  12811  pcprendvds  12856  pcprendvds2  12857  pcpremul  12859  pcdvdsb  12886  pcadd2  12907  pockthlem  12922  1arith  12933  4sqlem11  12967  4sqlem17  12973  ennnfonelemim  13038  bldisj  15118  perfect1  15715  lgsdilem2  15758  lgsne0  15760  lgseisenlem1  15792  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem1  15803  umgrnloop0  15961  bj-nnen2lp  16499  pwtrufal  16548  refeq  16582