Theorem pm2.65i 644

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 631	. 2 ⊢ (𝜑 → ¬ 𝜑)
4		pm2.01 621	. 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 619  ax-in2 620

This theorem is referenced by:  mt2  645  mto  668  pm5.19  713  noel  3498  0nelop  4340  elirr  4639  en2lp  4652  soirri  5131  canth  5969  0neqopab  6066  fzp1disj  10315  fzonel  10396  fzouzdisj  10417  4sqlem17  12982  lgsval2lem  15742  bj-imnimnn  16355  nnnotnotr  16606