Axiom ax-2 7

Description: Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature; see Proposition 2 of [Frege1879] p. 26. 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 390. (Contributed by NM, 30-Sep-1992.)

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  14  idALT  23  a2d  29  dfbi1ALT  214  imdi  389  sbi1  2071  difin0ss  4373  bj-sblem1  36843  bj-sblem2  36844  rp-fakeimass  43525  natlocalincr  46891  adh-minim  47013  adh-minimp  47025