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  3028  neldifsn  3801  nvel  4220  nlim0  4489  snnex  4543  onprc  4648  dtruex  4655  ordsoexmid  4658  nprrel  4769  0xp  4804  iprc  4999  son2lpi  5131  nfunv  5357  0fv  5673  canth  5964  acexmidlema  6004  acexmidlemb  6005  acexmidlemab  6007  mpo0  6086  php5dom  7044  1ndom2  7046  fi0  7165  pw1ne1  7437  pw1ne3  7438  sucpw1nel3  7441  3nelsucpw1  7442  0nnq  7574  0npr  7693  1ne0sr  7976  pnfnre  8211  mnfnre  8212  ine0  8563  inelr  8754  nn0nepnf  9463  1nuz2  9830  0nrp  9914  inftonninf  10694  lsw0  11151  eirr  12330  odd2np1  12424  n2dvds1  12463  1nprm  12676  structcnvcnv  13088  fvsetsid  13106  fnpr2ob  13413  0g0  13449  0ntop  14721  topnex  14800  umgredgnlp  15991  bj-nvel  16428  pw1ninf  16526  pwle2  16535  exmidsbthrlem  16562  trirec0xor  16585