Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > id | Structured version Visualization version GIF version |
Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 23. Its associated inference, idi 2, requires no axioms for its proof, contrary to id 22. (Contributed by NM, 29-Dec-1992.) (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 15 | 1 ⊢ (𝜑 → 𝜑) |
Copyright terms: Public domain | W3C validator |