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 41369
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 34719 . 2 wff ((𝜑𝜓) → (𝜑𝜒))
71, 4, 6bj-0 34719 1 wff ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  rp-frege3g  41372  frege3  41373  rp-misc1-frege  41374  rp-frege24  41375  rp-frege4g  41376  frege4  41377  rp-7frege  41379  rp-8frege  41382  frege39  41420  frege73  41514  frege79  41520
  Copyright terms: Public domain W3C validator