Axiom ax-frege52a 43819

Description: The case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we substitute the content of 𝜑 is affirmed (in this specific case the identity logical function) and the same proposition, this time where we substituted the content of 𝜓, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-frege52a	⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))

Detailed syntax breakdown of Axiom ax-frege52a

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wb 206	. 2 wff (𝜑 ↔ 𝜓)
4		wth	. . . 4 wff 𝜃
5		wch	. . . 4 wff 𝜒
6	1, 4, 5	wif 1063	. . 3 wff if-(𝜑, 𝜃, 𝜒)
7	2, 4, 5	wif 1063	. . 3 wff if-(𝜓, 𝜃, 𝜒)
8	6, 7	wi 4	. 2 wff (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))
9	3, 8	wi 4	1 wff ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))

This axiom is referenced by:  frege52aid  43820  frege53a  43822  frege57a  43835