Theorem mto 651

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  659  pm3.2ni  802  pm5.16  813  intnan  914  intnanr  915  equidqe  1512  nexr  1670  ru  2908  neldifsn  3653  nvel  4061  nlim0  4316  snnex  4369  onprc  4467  dtruex  4474  ordsoexmid  4477  nprrel  4584  0xp  4619  iprc  4807  son2lpi  4935  nfunv  5156  0fv  5456  acexmidlema  5765  acexmidlemb  5766  acexmidlemab  5768  mpo0  5841  php5dom  6757  fi0  6863  0nnq  7172  0npr  7291  1ne0sr  7574  pnfnre  7807  mnfnre  7808  ine0  8156  inelr  8346  nn0nepnf  9048  1nuz2  9400  0nrp  9477  inftonninf  10214  eirr  11485  odd2np1  11570  n2dvds1  11609  1nprm  11795  structcnvcnv  11975  fvsetsid  11993  0ntop  12174  topnex  12255  bj-nnst  12964  bj-nvel  13095  pwle2  13193  exmidsbthrlem  13217