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 43799
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 43780, and ax-frege2 43781. (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 36525 1 wff ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  frege26  43800  frege9  43802  frege12  43803  frege10  43810  frege17  43811  frege38  43831  frege53aid  43849  frege53a  43850  frege62a  43870  frege66a  43874  frege53b  43880  frege62b  43897  frege66b  43901  frege53c  43904  frege62c  43915  frege66c  43919  frege74  43927  frege84  43937  frege96  43949
  Copyright terms: Public domain W3C validator