Theorem mto 666

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 642	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:  mtbi  674  pm3.2ni  818  pm5.16  833  intnan  934  intnanr  935  equidqe  1578  nexr  1738  ru  3027  neldifsn  3798  nvel  4217  nlim0  4485  snnex  4539  onprc  4644  dtruex  4651  ordsoexmid  4654  nprrel  4764  0xp  4799  iprc  4993  son2lpi  5125  nfunv  5351  0fv  5667  canth  5958  acexmidlema  5998  acexmidlemb  5999  acexmidlemab  6001  mpo0  6080  php5dom  7032  1ndom2  7034  fi0  7153  pw1ne1  7425  pw1ne3  7426  sucpw1nel3  7429  3nelsucpw1  7430  0nnq  7562  0npr  7681  1ne0sr  7964  pnfnre  8199  mnfnre  8200  ine0  8551  inelr  8742  nn0nepnf  9451  1nuz2  9813  0nrp  9897  inftonninf  10676  lsw0  11132  eirr  12305  odd2np1  12399  n2dvds1  12438  1nprm  12651  structcnvcnv  13063  fvsetsid  13081  fnpr2ob  13388  0g0  13424  0ntop  14696  topnex  14775  umgredgnlp  15965  bj-nvel  16315  pw1ninf  16414  pwle2  16423  exmidsbthrlem  16450  trirec0xor  16473