Theorem mto 664

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 640	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  672  pm3.2ni  815  pm5.16  830  intnan  931  intnanr  932  equidqe  1556  nexr  1716  ru  3001  neldifsn  3769  nvel  4188  nlim0  4454  snnex  4508  onprc  4613  dtruex  4620  ordsoexmid  4623  nprrel  4733  0xp  4768  iprc  4961  son2lpi  5093  nfunv  5318  0fv  5630  canth  5915  acexmidlema  5953  acexmidlemb  5954  acexmidlemab  5956  mpo0  6033  php5dom  6980  1ndom2  6982  fi0  7098  pw1ne1  7370  pw1ne3  7371  sucpw1nel3  7374  3nelsucpw1  7375  0nnq  7507  0npr  7626  1ne0sr  7909  pnfnre  8144  mnfnre  8145  ine0  8496  inelr  8687  nn0nepnf  9396  1nuz2  9757  0nrp  9841  inftonninf  10619  lsw0  11073  eirr  12175  odd2np1  12269  n2dvds1  12308  1nprm  12521  structcnvcnv  12933  fvsetsid  12951  fnpr2ob  13257  0g0  13293  0ntop  14564  topnex  14643  umgredgnlp  15826  bj-nvel  16002  pwle2  16107  exmidsbthrlem  16133  trirec0xor  16156