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  1555  nexr  1715  ru  2997  neldifsn  3763  nvel  4177  nlim0  4441  snnex  4495  onprc  4600  dtruex  4607  ordsoexmid  4610  nprrel  4720  0xp  4755  iprc  4947  son2lpi  5079  nfunv  5304  0fv  5612  canth  5897  acexmidlema  5935  acexmidlemb  5936  acexmidlemab  5938  mpo0  6015  php5dom  6960  fi0  7077  pw1ne1  7341  pw1ne3  7342  sucpw1nel3  7345  3nelsucpw1  7346  0nnq  7477  0npr  7596  1ne0sr  7879  pnfnre  8114  mnfnre  8115  ine0  8466  inelr  8657  nn0nepnf  9366  1nuz2  9727  0nrp  9811  inftonninf  10587  lsw0  11041  eirr  12090  odd2np1  12184  n2dvds1  12223  1nprm  12436  structcnvcnv  12848  fvsetsid  12866  fnpr2ob  13172  0g0  13208  0ntop  14479  topnex  14558  bj-nvel  15833  pwle2  15935  exmidsbthrlem  15961  trirec0xor  15984