| 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 43803, and ax-frege2 43804. (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 36543 | 1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: frege26 43823 frege9 43825 frege12 43826 frege10 43833 frege17 43834 frege38 43854 frege53aid 43872 frege53a 43873 frege62a 43893 frege66a 43897 frege53b 43903 frege62b 43920 frege66b 43924 frege53c 43927 frege62c 43938 frege66c 43942 frege74 43950 frege84 43960 frege96 43972 |
| Copyright terms: Public domain | W3C validator |