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  1512  nexr  1672  ru  2936  neldifsn  3689  nvel  4097  nlim0  4353  snnex  4406  onprc  4509  dtruex  4516  ordsoexmid  4519  nprrel  4628  0xp  4663  iprc  4851  son2lpi  4979  nfunv  5200  0fv  5500  acexmidlema  5809  acexmidlemb  5810  acexmidlemab  5812  mpo0  5885  php5dom  6801  fi0  6912  pw1ne1  7147  pw1ne3  7148  sucpw1nel3  7151  3nelsucpw1  7152  0nnq  7267  0npr  7386  1ne0sr  7669  pnfnre  7902  mnfnre  7903  ine0  8252  inelr  8442  nn0nepnf  9144  1nuz2  9499  0nrp  9578  inftonninf  10322  eirr  11657  odd2np1  11745  n2dvds1  11784  1nprm  11971  structcnvcnv  12166  fvsetsid  12184  0ntop  12365  topnex  12446  bj-nnst  13291  bj-nvel  13432  pwle2  13531  exmidsbthrlem  13556  trirec0xor  13579