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  7312  pw1ne3  7313  sucpw1nel3  7316  3nelsucpw1  7317  0nnq  7448  0npr  7567  1ne0sr  7850  pnfnre  8085  mnfnre  8086  ine0  8437  inelr  8628  nn0nepnf  9337  1nuz2  9697  0nrp  9781  inftonninf  10551  eirr  11961  odd2np1  12055  n2dvds1  12094  1nprm  12307  structcnvcnv  12719  fvsetsid  12737  fnpr2ob  13042  0g0  13078  0ntop  14327  topnex  14406  bj-nvel  15627  pwle2  15729  exmidsbthrlem  15753  trirec0xor  15776