![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > falimtru | Structured version Visualization version GIF version |
Description: A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using falim 1671 instead of trud 1664 but the present proof using trud 1664 emphasizes that the result does not require the principle of explosion. (Proof modification is discouraged.) |
Ref | Expression |
---|---|
falimtru | ⊢ ((⊥ → ⊤) ↔ ⊤) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trud 1664 | . 2 ⊢ (⊥ → ⊤) | |
2 | 1 | bitru 1663 | 1 ⊢ ((⊥ → ⊤) ↔ ⊤) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ⊤wtru 1654 ⊥wfal 1666 |
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 199 df-tru 1657 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |