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  2760  sspssn  3045  neldifsn  3494  nvel  3886  nlim0  4118  snnex  4168  onprc  4261  dtruex  4268  ordsoexmid  4271  nprrel  4364  0xp  4398  iprc  4578  son2lpi  4699  nfunv  4911  0fv  5186  acexmidlema  5481  acexmidlemb  5482  acexmidlemab  5484  mpt20  5552  php5dom  6303  0nnq  6434  0npr  6553  1ne0sr  6823  pnfnre  7038  mnfnre  7039  ine0  7361  inelr  7542  1nuz2  8506  0nrp  8578  bj-nvel  9881