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  1546  nexr  1706  ru  2988  neldifsn  3753  nvel  4167  nlim0  4430  snnex  4484  onprc  4589  dtruex  4596  ordsoexmid  4599  nprrel  4709  0xp  4744  iprc  4935  son2lpi  5067  nfunv  5292  0fv  5597  canth  5878  acexmidlema  5916  acexmidlemb  5917  acexmidlemab  5919  mpo0  5996  php5dom  6933  fi0  7050  pw1ne1  7314  pw1ne3  7315  sucpw1nel3  7318  3nelsucpw1  7319  0nnq  7450  0npr  7569  1ne0sr  7852  pnfnre  8087  mnfnre  8088  ine0  8439  inelr  8630  nn0nepnf  9339  1nuz2  9699  0nrp  9783  inftonninf  10553  eirr  11963  odd2np1  12057  n2dvds1  12096  1nprm  12309  structcnvcnv  12721  fvsetsid  12739  fnpr2ob  13044  0g0  13080  0ntop  14351  topnex  14430  bj-nvel  15651  pwle2  15753  exmidsbthrlem  15779  trirec0xor  15802