This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: AxiomSimp. Axiom A1 of Margaris p. 49. One of the 3 axioms of propositional calculus. The 3 axioms are also given as Definition 2.1 of Hamilton p. 28. This axiom is calledSimp or "the principle of simplification" inPrincipia Mathematica (Theorem *2.02 of WhiteheadRussell p. 100) because "it enables us to pass from the joint assertion of ph and ps to the assertion of ph simply". It is Proposition 1 of Frege1879 p. 26, its first axiom. (Contributed by NM, 30-Sep-1992)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-1 | |- ( ph -> ( ps -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | |- ph |
|
| 1 | wps | |- ps |
|
| 2 | 1 0 | wi | |- ( ps -> ph ) |
| 3 | 0 2 | wi | |- ( ph -> ( ps -> ph ) ) |