Theorem mto 668

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 619  ax-in2 620

This theorem is referenced by:  mtbi  677  pm3.2ni  821  pm5.16  836  intnan  937  intnanr  938  equidqe  1581  nexr  1740  ru  3044  neldifsn  3828  nvel  4248  nlim0  4520  snnex  4574  onprc  4679  dtruex  4686  ordsoexmid  4689  nprrel  4800  0xp  4835  iprc  5031  son2lpi  5164  nfunv  5390  0fv  5713  canth  6009  acexmidlema  6049  acexmidlemb  6050  acexmidlemab  6052  mpo0  6131  php5dom  7130  1ndom2  7132  fi0  7275  pw1ne1  7552  pw1ne3  7553  sucpw1nel3  7556  3nelsucpw1  7557  0nnq  7695  0npr  7814  1ne0sr  8097  pnfnre  8331  mnfnre  8332  ine0  8684  inelr  8875  nn0nepnf  9588  1nuz2  9956  0nrp  10040  inftonninf  10828  lsw0  11297  eirr  12490  odd2np1  12584  n2dvds1  12623  1nprm  12836  ballotfilem2  13172  structcnvcnv  13312  fvsetsid  13330  fnpr2ob  13604  0g0  13639  0ntop  14998  topnex  15077  umgredgnlp  16273  konigsberg  16614  bj-nvel  16793  pw1ninf  16891  pwle2  16898  exmidsbthrlem  16928  trirec0xor  16955