Axiom ax-frege2 38085

Description: If a proposition ch is a necessary consequence of two propositions ps and ph and one of those, ps, is in turn a necessary consequence of the other, ph, then the proposition ch is a necessary consequence of the latter one, ph, 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	|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )

Detailed syntax breakdown of Axiom ax-frege2

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	2, 3	wi 4	. 2 wff ( ps -> ch )
5	1, 3	wi 4	. . 3 wff ( ph -> ch )
6	1, 2, 5	bj-0 32533	. 2 wff ( ( ph -> ps ) -> ( ph -> ch ) )
7	1, 4, 6	bj-0 32533	1 wff ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )

This axiom is referenced by:  rp-frege3g  38088  frege3  38089  rp-misc1-frege  38090  rp-frege24  38091  rp-frege4g  38092  frege4  38093  rp-7frege  38095  rp-8frege  38098  frege39  38136  frege73  38230  frege79  38236