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 36922
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 87 which can be proved from only ax-mp 5, ax-frege1 36903, and ax-frege2 36904. (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 31505 1 wff ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  frege26  36923  frege9  36925  frege12  36926  frege10  36933  frege17  36934  frege38  36954  frege53aid  36972  frege53a  36973  frege62a  36993  frege66a  36997  frege53b  37003  frege62b  37020  frege66b  37024  frege53c  37027  frege62c  37038  frege66c  37042  frege74  37050  frege84  37060  frege96  37072
  Copyright terms: Public domain W3C validator