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 40143, and ax-frege2 40144. (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 33883 | 1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege26 40163 frege9 40165 frege12 40166 frege10 40173 frege17 40174 frege38 40194 frege53aid 40212 frege53a 40213 frege62a 40233 frege66a 40237 frege53b 40243 frege62b 40260 frege66b 40264 frege53c 40267 frege62c 40278 frege66c 40282 frege74 40290 frege84 40300 frege96 40312 |
Copyright terms: Public domain | W3C validator |