![]() |
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 43780, and ax-frege2 43781. (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 36525 | 1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege26 43800 frege9 43802 frege12 43803 frege10 43810 frege17 43811 frege38 43831 frege53aid 43849 frege53a 43850 frege62a 43870 frege66a 43874 frege53b 43880 frege62b 43897 frege66b 43901 frege53c 43904 frege62c 43915 frege66c 43919 frege74 43927 frege84 43937 frege96 43949 |
Copyright terms: Public domain | W3C validator |