![]() |
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 42541, and ax-frege2 42542. (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 35418 | 1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
This axiom is referenced by: frege26 42561 frege9 42563 frege12 42564 frege10 42571 frege17 42572 frege38 42592 frege53aid 42610 frege53a 42611 frege62a 42631 frege66a 42635 frege53b 42641 frege62b 42658 frege66b 42662 frege53c 42665 frege62c 42676 frege66c 42680 frege74 42688 frege84 42698 frege96 42710 |
Copyright terms: Public domain | W3C validator |