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

Axiom ax-frege2 40423
Description: If a proposition 𝜒 is a necessary consequence of two propositions 𝜓 and 𝜑 and one of those, 𝜓, is in turn a necessary consequence of the other, 𝜑, then the proposition 𝜒 is a necessary consequence of the latter one, 𝜑, alone. Axiom 2 of [Frege1879] p. 26. Identical to ax-2 7. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
Assertion
Ref Expression
ax-frege2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))

Detailed syntax breakdown of Axiom ax-frege2
StepHypRef Expression
1 wph . 2 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
42, 3wi 4 . 2 wff (𝜓𝜒)
51, 3wi 4 . . 3 wff (𝜑𝜒)
61, 2, 5bj-0 33955 . 2 wff ((𝜑𝜓) → (𝜑𝜒))
71, 4, 6bj-0 33955 1 wff ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  rp-frege3g  40426  frege3  40427  rp-misc1-frege  40428  rp-frege24  40429  rp-frege4g  40430  frege4  40431  rp-7frege  40433  rp-8frege  40436  frege39  40474  frege73  40568  frege79  40574
  Copyright terms: Public domain W3C validator