Axiom ax-frege2

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 . (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-frege2	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	1 2	wi	⊢ ( 𝜓 → 𝜒 )
4	0 3	wi	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
5	0 1	wi	⊢ ( 𝜑 → 𝜓 )
6	0 2	wi	⊢ ( 𝜑 → 𝜒 )
7	5 6	wi	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) )
8	4 7	wi	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )