Description: AxiomFrege. 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 asFrege 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 . (Contributed by NM, 30-Sep-1992)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-2 | |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | |- ph |
|
| 1 | wps | |- ps |
|
| 2 | wch | |- ch |
|
| 3 | 1 2 | wi | |- ( ps -> ch ) |
| 4 | 0 3 | wi | |- ( ph -> ( ps -> ch ) ) |
| 5 | 0 1 | wi | |- ( ph -> ps ) |
| 6 | 0 2 | wi | |- ( ph -> ch ) |
| 7 | 5 6 | wi | |- ( ( ph -> ps ) -> ( ph -> ch ) ) |
| 8 | 4 7 | wi | |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) |