Theorem mto 666

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  674  pm3.2ni  818  pm5.16  833  intnan  934  intnanr  935  equidqe  1578  nexr  1738  ru  3027  neldifsn  3798  nvel  4217  nlim0  4486  snnex  4540  onprc  4645  dtruex  4652  ordsoexmid  4655  nprrel  4766  0xp  4801  iprc  4996  son2lpi  5128  nfunv  5354  0fv  5670  canth  5961  acexmidlema  6001  acexmidlemb  6002  acexmidlemab  6004  mpo0  6083  php5dom  7037  1ndom2  7039  fi0  7158  pw1ne1  7430  pw1ne3  7431  sucpw1nel3  7434  3nelsucpw1  7435  0nnq  7567  0npr  7686  1ne0sr  7969  pnfnre  8204  mnfnre  8205  ine0  8556  inelr  8747  nn0nepnf  9456  1nuz2  9818  0nrp  9902  inftonninf  10681  lsw0  11137  eirr  12311  odd2np1  12405  n2dvds1  12444  1nprm  12657  structcnvcnv  13069  fvsetsid  13087  fnpr2ob  13394  0g0  13430  0ntop  14702  topnex  14781  umgredgnlp  15971  bj-nvel  16369  pw1ninf  16468  pwle2  16477  exmidsbthrlem  16504  trirec0xor  16527