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  714  noel  3514  0nelop  4366  elirr  4665  en2lp  4678  soirri  5159  canth  6003  0neqopab  6100  fczsupp0  6461  fzp1disj  10418  fzonel  10499  fzouzdisj  10520  hashfibclem  11210  4sqlem17  13109  lgsval2lem  15900  bj-imnimnn  16527  nnnotnotr  16777