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  12032  odd2np1  12126  n2dvds1  12165  1nprm  12378  structcnvcnv  12790  fvsetsid  12808  fnpr2ob  13114  0g0  13150  0ntop  14421  topnex  14500  bj-nvel  15766  pwle2  15868  exmidsbthrlem  15894  trirec0xor  15917