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 38420
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 38401, and ax-frege2 38402. (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 32658 1 wff ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  frege26  38421  frege9  38423  frege12  38424  frege10  38431  frege17  38432  frege38  38452  frege53aid  38470  frege53a  38471  frege62a  38491  frege66a  38495  frege53b  38501  frege62b  38518  frege66b  38522  frege53c  38525  frege62c  38536  frege66c  38540  frege74  38548  frege84  38558  frege96  38570
  Copyright terms: Public domain W3C validator