![]() |
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 42623, and ax-frege2 42624. (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 35504 | 1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege26 42643 frege9 42645 frege12 42646 frege10 42653 frege17 42654 frege38 42674 frege53aid 42692 frege53a 42693 frege62a 42713 frege66a 42717 frege53b 42723 frege62b 42740 frege66b 42744 frege53c 42747 frege62c 42758 frege66c 42762 frege74 42770 frege84 42780 frege96 42792 |
Copyright terms: Public domain | W3C validator |