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 42169
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 42150, and ax-frege2 42151. (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 35051 1 wff ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  frege26  42170  frege9  42172  frege12  42173  frege10  42180  frege17  42181  frege38  42201  frege53aid  42219  frege53a  42220  frege62a  42240  frege66a  42244  frege53b  42250  frege62b  42267  frege66b  42271  frege53c  42274  frege62c  42285  frege66c  42289  frege74  42297  frege84  42307  frege96  42319
  Copyright terms: Public domain W3C validator