Theorem mto 662

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  670  pm3.2ni  813  pm5.16  828  intnan  929  intnanr  930  equidqe  1532  nexr  1692  ru  2963  neldifsn  3724  nvel  4138  nlim0  4396  snnex  4450  onprc  4553  dtruex  4560  ordsoexmid  4563  nprrel  4673  0xp  4708  iprc  4897  son2lpi  5027  nfunv  5251  0fv  5552  canth  5831  acexmidlema  5868  acexmidlemb  5869  acexmidlemab  5871  mpo0  5947  php5dom  6865  fi0  6976  pw1ne1  7230  pw1ne3  7231  sucpw1nel3  7234  3nelsucpw1  7235  0nnq  7365  0npr  7484  1ne0sr  7767  pnfnre  8001  mnfnre  8002  ine0  8353  inelr  8543  nn0nepnf  9249  1nuz2  9608  0nrp  9691  inftonninf  10443  eirr  11788  odd2np1  11880  n2dvds1  11919  1nprm  12116  structcnvcnv  12480  fvsetsid  12498  fnpr2ob  12764  0g0  12800  0ntop  13546  topnex  13625  bj-nvel  14688  pwle2  14787  exmidsbthrlem  14809  trirec0xor  14832