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  7589  pw1ne3  7590  sucpw1nel3  7593  3nelsucpw1  7594  0nnq  7732  0npr  7851  1ne0sr  8134  pnfnre  8368  mnfnre  8369  ine0  8723  inelr  8915  nn0nepnf  9643  1nuz2  10016  0nrp  10101  inftonninf  10894  lsw0  11368  eirr  12565  odd2np1  12659  n2dvds1  12698  1nprm  12911  ballotfilem2  13280  structcnvcnv  13420  fvsetsid  13438  fnpr2ob  13714  0g0  13749  0ntop  15199  topnex  15278  umgredgnlp  16559  konigsberg  16900  bj-nvel  17089  pw1ninf  17187  pwle2  17194  wexmiddifxylem  17211  exmidsbthrlem  17233  trirec0xor  17261  alseu-no-surprise  17346