Theorem mto 663

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  671  pm3.2ni  814  pm5.16  829  intnan  930  intnanr  931  equidqe  1543  nexr  1703  ru  2984  neldifsn  3748  nvel  4162  nlim0  4425  snnex  4479  onprc  4584  dtruex  4591  ordsoexmid  4594  nprrel  4704  0xp  4739  iprc  4930  son2lpi  5062  nfunv  5287  0fv  5590  canth  5871  acexmidlema  5909  acexmidlemb  5910  acexmidlemab  5912  mpo0  5988  php5dom  6919  fi0  7034  pw1ne1  7289  pw1ne3  7290  sucpw1nel3  7293  3nelsucpw1  7294  0nnq  7424  0npr  7543  1ne0sr  7826  pnfnre  8061  mnfnre  8062  ine0  8413  inelr  8603  nn0nepnf  9311  1nuz2  9671  0nrp  9755  inftonninf  10513  eirr  11922  odd2np1  12014  n2dvds1  12053  1nprm  12252  structcnvcnv  12634  fvsetsid  12652  fnpr2ob  12923  0g0  12959  0ntop  14175  topnex  14254  bj-nvel  15389  pwle2  15489  exmidsbthrlem  15512  trirec0xor  15535