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  3797  nvel  4216  nlim0  4484  snnex  4538  onprc  4643  dtruex  4650  ordsoexmid  4653  nprrel  4763  0xp  4798  iprc  4992  son2lpi  5124  nfunv  5350  0fv  5664  canth  5951  acexmidlema  5991  acexmidlemb  5992  acexmidlemab  5994  mpo0  6073  php5dom  7020  1ndom2  7022  fi0  7138  pw1ne1  7410  pw1ne3  7411  sucpw1nel3  7414  3nelsucpw1  7415  0nnq  7547  0npr  7666  1ne0sr  7949  pnfnre  8184  mnfnre  8185  ine0  8536  inelr  8727  nn0nepnf  9436  1nuz2  9797  0nrp  9881  inftonninf  10659  lsw0  11114  eirr  12285  odd2np1  12379  n2dvds1  12418  1nprm  12631  structcnvcnv  13043  fvsetsid  13061  fnpr2ob  13368  0g0  13404  0ntop  14675  topnex  14754  umgredgnlp  15944  bj-nvel  16218  pwle2  16323  exmidsbthrlem  16349  trirec0xor  16372