![]() |
Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-frege8 | Structured version Visualization version GIF version |
Description: Swap antecedents. If two conditions have a proposition as a consequence, their order is immaterial. Third axiom of Frege's 1879 work but identical to pm2.04 90 which can be proved from only ax-mp 5, ax-frege1 42150, and ax-frege2 42151. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-frege8 | ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | wch | . . 3 wff 𝜒 | |
4 | 2, 3 | wi 4 | . 2 wff (𝜓 → 𝜒) |
5 | 1, 3 | wi 4 | . . 3 wff (𝜑 → 𝜒) |
6 | 2, 5 | wi 4 | . 2 wff (𝜓 → (𝜑 → 𝜒)) |
7 | 1, 4, 6 | bj-0 35051 | 1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege26 42170 frege9 42172 frege12 42173 frege10 42180 frege17 42181 frege38 42201 frege53aid 42219 frege53a 42220 frege62a 42240 frege66a 42244 frege53b 42250 frege62b 42267 frege66b 42271 frege53c 42274 frege62c 42285 frege66c 42289 frege74 42297 frege84 42307 frege96 42319 |
Copyright terms: Public domain | W3C validator |