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 Unicode version

Axiom ax-frege54a 38156

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 251. (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
2	1, 1	wb 196	1

Colors of variables: wff setvar class

This axiom is referenced by: frege54cor1a 38158