Theorem mto 657

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  665  pm3.2ni  808  pm5.16  823  intnan  924  intnanr  925  equidqe  1525  nexr  1685  ru  2954  neldifsn  3713  nvel  4122  nlim0  4379  snnex  4433  onprc  4536  dtruex  4543  ordsoexmid  4546  nprrel  4656  0xp  4691  iprc  4879  son2lpi  5007  nfunv  5231  0fv  5531  canth  5807  acexmidlema  5844  acexmidlemb  5845  acexmidlemab  5847  mpo0  5923  php5dom  6841  fi0  6952  pw1ne1  7206  pw1ne3  7207  sucpw1nel3  7210  3nelsucpw1  7211  0nnq  7326  0npr  7445  1ne0sr  7728  pnfnre  7961  mnfnre  7962  ine0  8313  inelr  8503  nn0nepnf  9206  1nuz2  9565  0nrp  9646  inftonninf  10397  eirr  11741  odd2np1  11832  n2dvds1  11871  1nprm  12068  structcnvcnv  12432  fvsetsid  12450  0g0  12630  0ntop  12799  topnex  12880  bj-nvel  13932  pwle2  14031  exmidsbthrlem  14054  trirec0xor  14077