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 38402
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 32658 . 2 wff ((𝜑𝜓) → (𝜑𝜒))
71, 4, 6bj-0 32658 1 wff ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
Colors of variables: wff setvar class
This axiom is referenced by:  rp-frege3g  38405  frege3  38406  rp-misc1-frege  38407  rp-frege24  38408  rp-frege4g  38409  frege4  38410  rp-7frege  38412  rp-8frege  38415  frege39  38453  frege73  38547  frege79  38553
  Copyright terms: Public domain W3C validator