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  8721  inelr  8912  nn0nepnf  9638  1nuz2  10006  0nrp  10090  inftonninf  10879  lsw0  11352  eirr  12546  odd2np1  12640  n2dvds1  12679  1nprm  12892  ballotfilem2  13228  structcnvcnv  13368  fvsetsid  13386  fnpr2ob  13661  0g0  13696  0ntop  15108  topnex  15187  umgredgnlp  16393  konigsberg  16734  bj-nvel  16923  pw1ninf  17021  pwle2  17028  wexmiddifxylem  17045  exmidsbthrlem  17067  trirec0xor  17094  alseu-no-surprise  17179