ax-frege54a - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-frege54a		Structured version Visualization version GIF version

Axiom ax-frege54a 41359

Description: Reflexive equality of wffs. The content of 𝜑 is identical with the content of 𝜑. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 260. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

**Assertion**
Ref	Expression
ax-frege54a	⊢ (𝜑 ↔ 𝜑)

**Detailed syntax breakdown of Axiom ax-frege54a**
Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2	1, 1	wb 205	1 wff (𝜑 ↔ 𝜑)

Colors of variables: wff setvar class

This axiom is referenced by: frege54cor1a 41361

W3C validator