Theorem falimfal 1567

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

Syntax hints:   → wi 4   ↔ wb 205  ⊤wtru 1542  ⊥wfal 1553

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 1544

This theorem is referenced by: (None)