Theorem mto 672

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  681  pm3.2ni  825  pm5.16  840  intnan  941  intnanr  942  equidqe  1585  nexr  1744  ru  3050  neldifsn  3839  nvel  4261  nlim0  4534  snnex  4589  onprc  4694  dtruex  4701  ordsoexmid  4704  nprrel  4815  0xp  4850  iprc  5046  son2lpi  5179  nfunv  5405  0fv  5728  canth  6026  acexmidlema  6066  acexmidlemb  6067  acexmidlemab  6069  mpo0  6148  php5dom  7154  1ndom2  7156  fi0  7299  pw1ne1  7578  pw1ne3  7579  sucpw1nel3  7582  3nelsucpw1  7583  0nnq  7721  0npr  7840  1ne0sr  8123  pnfnre  8357  mnfnre  8358  ine0  8711  inelr  8902  nn0nepnf  9617  1nuz2  9985  0nrp  10069  inftonninf  10857  lsw0  11330  eirr  12524  odd2np1  12618  n2dvds1  12657  1nprm  12870  ballotfilem2  13206  structcnvcnv  13346  fvsetsid  13364  fnpr2ob  13638  0g0  13673  0ntop  15031  topnex  15110  umgredgnlp  16307  konigsberg  16648  bj-nvel  16837  pw1ninf  16935  pwle2  16942  exmidsbthrlem  16972  trirec0xor  16999