Theorem falimtru 1594

Description: A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using falim 1586 instead of trud 1579 but the present proof using trud 1579 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 1579	. 2 ⊢ (⊥ → ⊤)
2	1	bitru 1578	1 ⊢ ((⊥ → ⊤) ↔ ⊤)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ⊤wtru 1570  ⊥wfal 1581

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1572

This theorem is used by: (None)