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 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mt2  649  mto  672  pm5.19  718  noel  3525  0nelop  4386  elirr  4686  en2lp  4699  soirri  5180  canth  6030  0neqopab  6127  fczsupp0  6493  fzp1disj  10470  fzonel  10551  fzouzdisj  10572  hashfibclem  11265  4sqlem17  13169  lgsval2lem  16112  bj-imnimnn  16749  nnnotnotr  16999  als-no-surprise  17121