Theorem pm2.65i 640

Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
pm2.65i.1	⊢ (𝜑 → 𝜓)
pm2.65i.2	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.65i	⊢ ¬ 𝜑

Proof of Theorem pm2.65i

Step	Hyp	Ref	Expression
1		pm2.65i.2	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl3 627	. 2 ⊢ (𝜑 → ¬ 𝜑)
4		pm2.01 617	. 2 ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
5	3, 4	ax-mp 5	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mt2  641  mto  663  pm5.19  707  noel  3446  0nelop  4273  elirr  4565  en2lp  4578  soirri  5048  canth  5859  0neqopab  5951  fzp1disj  10132  fzonel  10213  fzouzdisj  10233  4sqlem17  12519  lgsval2lem  15054  bj-imnimnn  15154  nnnotnotr  15406