Theorem pm2.65i 642

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 629	. 2 ⊢ (𝜑 → ¬ 𝜑)
4		pm2.01 619	. 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 617  ax-in2 618

This theorem is referenced by:  mt2  643  mto  666  pm5.19  710  noel  3475  0nelop  4313  elirr  4610  en2lp  4623  soirri  5099  canth  5925  0neqopab  6020  fzp1disj  10244  fzonel  10325  fzouzdisj  10346  4sqlem17  12896  lgsval2lem  15654  bj-imnimnn  16012  nnnotnotr  16263