Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-frege8 Structured version   Visualization version   GIF version

Axiom ax-frege8 42642
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.)
Assertion
Ref Expression
ax-frege8 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))

Detailed syntax breakdown of Axiom ax-frege8
StepHypRef Expression
1 wph . 2 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
42, 3wi 4 . 2 wff (𝜓𝜒)
51, 3wi 4 . . 3 wff (𝜑𝜒)
62, 5wi 4 . 2 wff (𝜓 → (𝜑𝜒))
71, 4, 6bj-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