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  1554  nexr  1714  ru  2996  neldifsn  3762  nvel  4176  nlim0  4440  snnex  4494  onprc  4599  dtruex  4606  ordsoexmid  4609  nprrel  4719  0xp  4754  iprc  4946  son2lpi  5078  nfunv  5303  0fv  5611  canth  5896  acexmidlema  5934  acexmidlemb  5935  acexmidlemab  5937  mpo0  6014  php5dom  6959  fi0  7076  pw1ne1  7340  pw1ne3  7341  sucpw1nel3  7344  3nelsucpw1  7345  0nnq  7476  0npr  7595  1ne0sr  7878  pnfnre  8113  mnfnre  8114  ine0  8465  inelr  8656  nn0nepnf  9365  1nuz2  9726  0nrp  9810  inftonninf  10585  lsw0  11039  eirr  12061  odd2np1  12155  n2dvds1  12194  1nprm  12407  structcnvcnv  12819  fvsetsid  12837  fnpr2ob  13143  0g0  13179  0ntop  14450  topnex  14529  bj-nvel  15795  pwle2  15897  exmidsbthrlem  15923  trirec0xor  15946