Theorem pm2.65i 648

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 635	. 2 ⊢ (𝜑 → ¬ 𝜑)
4		pm2.01 625	. 2 ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
5	3, 4	ax-mp 5	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mt2  649  mto  672  pm5.19  718  noel  3525  0nelop  4390  elirr  4690  en2lp  4703  soirri  5185  canth  6039  0neqopab  6136  fczsupp0  6503  fzp1disj  10505  fzonel  10586  fzouzdisj  10607  hashfibclem  11305  4sqlem17  13216  lgsval2lem  16346  bj-imnimnn  16983  nnnotnotr  17233  als-no-surprise  17366