Theorem mto 652

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  660  pm3.2ni  803  pm5.16  814  intnan  915  intnanr  916  equidqe  1513  nexr  1671  ru  2912  neldifsn  3661  nvel  4069  nlim0  4324  snnex  4377  onprc  4475  dtruex  4482  ordsoexmid  4485  nprrel  4592  0xp  4627  iprc  4815  son2lpi  4943  nfunv  5164  0fv  5464  acexmidlema  5773  acexmidlemb  5774  acexmidlemab  5776  mpo0  5849  php5dom  6765  fi0  6871  0nnq  7196  0npr  7315  1ne0sr  7598  pnfnre  7831  mnfnre  7832  ine0  8180  inelr  8370  nn0nepnf  9072  1nuz2  9427  0nrp  9506  inftonninf  10245  eirr  11521  odd2np1  11606  n2dvds1  11645  1nprm  11831  structcnvcnv  12014  fvsetsid  12032  0ntop  12213  topnex  12294  bj-nnst  13135  bj-nvel  13266  pwle2  13366  exmidsbthrlem  13392  trirec0xor  13413