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 39051
 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 33119 . 2 wff ((𝜑𝜓) → (𝜑𝜒))
71, 4, 6bj-0 33119 1 wff ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
 Colors of variables: wff setvar class This axiom is referenced by:  rp-frege3g  39054  frege3  39055  rp-misc1-frege  39056  rp-frege24  39057  rp-frege4g  39058  frege4  39059  rp-7frege  39061  rp-8frege  39064  frege39  39102  frege73  39196  frege79  39202
 Copyright terms: Public domain W3C validator