Axiom ax-frege2 44776

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

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	2, 3	wi 4	. 2 wff (𝜓 → 𝜒)
5	1, 3	wi 4	. . 3 wff (𝜑 → 𝜒)
6	1, 2, 5	bj-0 37388	. 2 wff ((𝜑 → 𝜓) → (𝜑 → 𝜒))
7	1, 4, 6	bj-0 37388	1 wff ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

This axiom is used by:  rp-frege3g  44779  frege3  44780  rp-misc1-frege  44781  rp-frege24  44782  rp-frege4g  44783  frege4  44784  rp-7frege  44786  rp-8frege  44789  frege39  44827  frege73  44921  frege79  44927