Axiom ax-L2 12

Description: Axiom of Frege.

Assertion

Ref	Expression
ax-L2	⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

Detailed syntax breakdown of Axiom ax-L2

Step	Hyp	Ref	Expression
1		wff-ph	. . 3 wff 𝜑
2		wff-ps	. . . 4 wff 𝜓
3		wff-ch	. . . 4 wff 𝜒
4	2, 3	wff-imp 10	. . 3 wff (𝜓 → 𝜒)
5	1, 4	wff-imp 10	. 2 wff (𝜑 → (𝜓 → 𝜒))
6	1, 2	wff-imp 10	. . 3 wff (𝜑 → 𝜓)
7	1, 3	wff-imp 10	. . 3 wff (𝜑 → 𝜒)
8	6, 7	wff-imp 10	. 2 wff ((𝜑 → 𝜓) → (𝜑 → 𝜒))
9	5, 8	wff-imp 10	1 wff ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

This axiom is referenced by:  axL2.SH  31  rae-P1.5  37  rcp-FR1  39  rcp-FR2  41  rcp-FR3  43  axL2.AC.SH  46  imcomm-P1.6  48