Theorem mto 672

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mtbi  681  pm3.2ni  825  pm5.16  840  intnan  941  intnanr  942  equidqe  1585  nexr  1744  ru  3050  neldifsn  3844  nvel  4266  nlim0  4539  snnex  4594  onprc  4699  dtruex  4706  ordsoexmid  4709  nprrel  4820  0xp  4855  iprc  5051  son2lpi  5184  nfunv  5410  0fv  5734  canth  6036  acexmidlema  6076  acexmidlemb  6077  acexmidlemab  6079  mpo0  6158  php5dom  7164  1ndom2  7166  fi0  7309  pw1ne1  7588  pw1ne3  7589  sucpw1nel3  7592  3nelsucpw1  7593  0nnq  7731  0npr  7850  1ne0sr  8133  pnfnre  8367  mnfnre  8368  ine0  8722  inelr  8914  nn0nepnf  9642  1nuz2  10015  0nrp  10100  inftonninf  10892  lsw0  11366  eirr  12562  odd2np1  12656  n2dvds1  12695  1nprm  12908  ballotfilem2  13277  structcnvcnv  13417  fvsetsid  13435  fnpr2ob  13710  0g0  13745  0ntop  15157  topnex  15236  umgredgnlp  16491  konigsberg  16832  bj-nvel  17021  pw1ninf  17119  pwle2  17126  wexmiddifxylem  17143  exmidsbthrlem  17165  trirec0xor  17192  alseu-no-surprise  17277