Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > truimtru | Structured version Visualization version GIF version |
Description: A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using trud 1547 instead of id 22 but the principle of identity id 22 is more basic, and the present proof indicates that the result still holds in relevance logic. (Proof modification is discouraged.) |
Ref | Expression |
---|---|
truimtru | ⊢ ((⊤ → ⊤) ↔ ⊤) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (⊤ → ⊤) | |
2 | 1 | bitru 1546 | 1 ⊢ ((⊤ → ⊤) ↔ ⊤) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ⊤wtru 1538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 209 df-tru 1540 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |