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 395. (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  217  imdi  394  sbi1  2079  difin0ss  4300  bj-sblem1  34928  bj-sblem2  34929  rp-fakeimass  40989  adh-minim  44356  adh-minimp  44368