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  679  mtbird  680  pwntru  4311  po2nr  4429  po3nr  4430  sotricim  4443  elirr  4662  ordn2lp  4666  en2lp  4675  fvdifsuppst  6443  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  nndomo  7117  fnfi  7202  difinfsnlem  7389  nninfwlpoimlemginf  7466  2omotaplemap  7567  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  caucvgprlemladdrl  7989  caucvgprprlemaddq  8019  msqge0  8886  mulge0  8889  squeeze0  9174  elnn0z  9586  fznlem  10371  frec2uzf1od  10764  seqf1oglem1  10877  facndiv  11097  sumrbdclem  12056  prodrbdclem  12250  alzdvds  12533  fzm1ndvds  12535  fzo0dvdseq  12536  bitsfzolem  12633  bitsfzo  12634  rpdvds  12789  nonsq  12897  prmdiv  12925  odzdvds  12936  pcprendvds  12981  pcprendvds2  12982  pcpremul  12984  pcdvdsb  13011  pcadd2  13032  pockthlem  13047  1arith  13058  4sqlem11  13092  4sqlem17  13098  ennnfonelemim  13164  bldisj  15253  perfect1  15853  lgsdilem2  15896  lgsne0  15898  lgseisenlem1  15930  lgseisenlem2  15931  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2lem1  15941  umgrnloop0  16099  bj-nnen2lp  16711  pwtrufal  16758  refeq  16795