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  5969  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  mpo0  6091  php5dom  7049  1ndom2  7051  fi0  7174  pw1ne1  7447  pw1ne3  7448  sucpw1nel3  7451  3nelsucpw1  7452  0nnq  7584  0npr  7703  1ne0sr  7986  pnfnre  8221  mnfnre  8222  ine0  8573  inelr  8764  nn0nepnf  9473  1nuz2  9840  0nrp  9924  inftonninf  10705  lsw0  11165  eirr  12345  odd2np1  12439  n2dvds1  12478  1nprm  12691  structcnvcnv  13103  fvsetsid  13121  fnpr2ob  13428  0g0  13464  0ntop  14737  topnex  14816  umgredgnlp  16009  bj-nvel  16518  pw1ninf  16616  pwle2  16625  exmidsbthrlem  16652  trirec0xor  16675