Theorem mto 620

Description: The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mto.1	⊢ ¬ 𝜓
mto.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mto	⊢ ¬ 𝜑

Proof of Theorem mto

Step	Hyp	Ref	Expression
1		mto.2	. 2 ⊢ (𝜑 → 𝜓)
2		mto.1	. . 3 ⊢ ¬ 𝜓
3	2	a1i 9	. 2 ⊢ (𝜑 → ¬ 𝜓)
4	1, 3	pm2.65i 600	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  627  pm3.2ni  759  pm5.16  770  intnan  871  intnanr  872  equidqe  1465  nexr  1622  ru  2814  neldifsn  3519  nvel  3910  nlim0  4149  snnex  4199  onprc  4295  dtruex  4302  ordsoexmid  4305  nprrel  4404  0xp  4438  iprc  4618  son2lpi  4741  nfunv  4953  0fv  5229  acexmidlema  5523  acexmidlemb  5524  acexmidlemab  5526  mpt20  5594  php5dom  6349  0nnq  6554  0npr  6673  1ne0sr  6943  pnfnre  7160  mnfnre  7161  ine0  7498  inelr  7684  1nuz2  8693  0nrp  8767  odd2np1  10272  n2dvds1  10312  1nprm  10496  bj-nvel  10688