| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > id | GIF version | ||
| Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.) |
| Ref | Expression |
|---|---|
| id | ⊢ (𝜑 → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1 6 | . 2 ⊢ (𝜑 → (𝜑 → 𝜑)) | |
| 2 | ax-1 6 | . 2 ⊢ (𝜑 → ((𝜑 → 𝜑) → 𝜑)) | |
| 3 | 1, 2 | mpd 13 | 1 ⊢ (𝜑 → 𝜑) |
| Copyright terms: Public domain | W3C validator |