![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.65i | GIF version |
Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Ref | Expression |
---|---|
pm2.65i.1 | ⊢ (𝜑 → 𝜓) |
pm2.65i.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.65i | ⊢ ¬ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.65i.2 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
2 | pm2.65i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | nsyl3 627 | . 2 ⊢ (𝜑 → ¬ 𝜑) |
4 | pm2.01 617 | . 2 ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) | |
5 | 3, 4 | ax-mp 5 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 615 ax-in2 616 |
This theorem is referenced by: mt2 641 mto 663 pm5.19 707 noel 3441 0nelop 4266 elirr 4558 en2lp 4571 soirri 5041 canth 5849 0neqopab 5940 fzp1disj 10109 fzonel 10189 fzouzdisj 10209 4sqlem17 12438 lgsval2lem 14864 bj-imnimnn 14943 nnnotnotr 15195 |
Copyright terms: Public domain | W3C validator |