Theorem falimtru 1565

Description: A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using falim 1557 instead of trud 1550 but the present proof using trud 1550 emphasizes that the result does not require the principle of explosion. (Proof modification is discouraged.)

Assertion

Ref	Expression
falimtru	⊢ ((⊥ → ⊤) ↔ ⊤)

Proof of Theorem falimtru

Step	Hyp	Ref	Expression
1		trud 1550	. 2 ⊢ (⊥ → ⊤)
2	1	bitru 1549	1 ⊢ ((⊥ → ⊤) ↔ ⊤)

Syntax hints:   → wi 4   ↔ wb 205  ⊤wtru 1541  ⊥wfal 1552

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 206  df-tru 1543

This theorem is referenced by: (None)