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 38603
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 32872 . 2 wff ((𝜑𝜓) → (𝜑𝜒))
71, 4, 6bj-0 32872 1 wff ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  rp-frege3g  38606  frege3  38607  rp-misc1-frege  38608  rp-frege24  38609  rp-frege4g  38610  frege4  38611  rp-7frege  38613  rp-8frege  38616  frege39  38654  frege73  38748  frege79  38754
  Copyright terms: Public domain W3C validator