Theorem mto 588

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbi  595  pm3.2ni  726  pm5.16  737  intnan  838  intnanr  839  equidqe  1425  nexr  1582  ru  2763  sspssn  3048  neldifsn  3497  nvel  3889  nlim0  4131  snnex  4181  onprc  4276  dtruex  4283  ordsoexmid  4286  nprrel  4386  0xp  4420  iprc  4600  son2lpi  4721  nfunv  4933  0fv  5208  acexmidlema  5503  acexmidlemb  5504  acexmidlemab  5506  mpt20  5574  php5dom  6325  0nnq  6462  0npr  6581  1ne0sr  6851  pnfnre  7067  mnfnre  7068  ine0  7391  inelr  7575  1nuz2  8543  0nrp  8616  bj-nvel  10017