Axiom ax-2 7

Description: Axiom Frege. Axiom A2 of [Margaris] p. 49. This axiom "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 250. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Detailed syntax breakdown of Axiom ax-2

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

This axiom is referenced by:  a2i  11  idALT  20  a2d  26  imdi  249  sbi1v  1884  ralim  2529