Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-frege52a | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ax-frege52a | ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wb 209 | . 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-(𝜓, 𝜃, 𝜒))) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege52aid 41143 frege53a 41145 frege57a 41158 |
Copyright terms: Public domain | W3C validator |