Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-frege58a | Structured version Visualization version GIF version |
Description: If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2071. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-frege58a | ⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wps | . . 3 wff 𝜓 | |
2 | wch | . . 3 wff 𝜒 | |
3 | 1, 2 | wa 396 | . 2 wff (𝜓 ∧ 𝜒) |
4 | wph | . . 3 wff 𝜑 | |
5 | 4, 1, 2 | wif 1060 | . 2 wff if-(𝜑, 𝜓, 𝜒) |
6 | 3, 5 | wi 4 | 1 wff ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege58acor 41465 frege61a 41468 frege67a 41474 |
Copyright terms: Public domain | W3C validator |