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  676  pm3.2ni  820  pm5.16  835  intnan  936  intnanr  937  equidqe  1580  nexr  1740  ru  3030  neldifsn  3803  nvel  4222  nlim0  4491  snnex  4545  onprc  4650  dtruex  4657  ordsoexmid  4660  nprrel  4771  0xp  4806  iprc  5001  son2lpi  5133  nfunv  5359  0fv  5677  canth  5968  acexmidlema  6008  acexmidlemb  6009  acexmidlemab  6011  mpo0  6090  php5dom  7048  1ndom2  7050  fi0  7173  pw1ne1  7446  pw1ne3  7447  sucpw1nel3  7450  3nelsucpw1  7451  0nnq  7583  0npr  7702  1ne0sr  7985  pnfnre  8220  mnfnre  8221  ine0  8572  inelr  8763  nn0nepnf  9472  1nuz2  9839  0nrp  9923  inftonninf  10703  lsw0  11160  eirr  12339  odd2np1  12433  n2dvds1  12472  1nprm  12685  structcnvcnv  13097  fvsetsid  13115  fnpr2ob  13422  0g0  13458  0ntop  14730  topnex  14809  umgredgnlp  16002  bj-nvel  16492  pw1ninf  16590  pwle2  16599  exmidsbthrlem  16626  trirec0xor  16649