Definition df-fal 1320

Description: Definition of ⊥, a contradiction. ⊥ is a constant false. (Contributed by Anthony Hart, 22-Oct-2010.)

Assertion

Ref	Expression
df-fal	⊢ ( ⊥ ↔ ¬ ⊤ )

Detailed syntax breakdown of Definition df-fal

Step	Hyp	Ref	Expression
1		wfal 1317	. 2 wff ⊥
2		wtru 1316	. . 3 wff ⊤
3	2	wn 3	. 2 wff ¬ ⊤
4	1, 3	wb 176	1 wff ( ⊥ ↔ ¬ ⊤ )

This definition is referenced by:  fal  1322  nottru  1348