Theorem falimfal 1596

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

Assertion

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

Proof of Theorem falimfal

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (⊥ → ⊥)
2	1	bitru 1579	1 ⊢ ((⊥ → ⊥) ↔ ⊤)

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

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 1573

This theorem is used by: (None)