Axiom ax-1

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	⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	1 0	wi	⊢ ( 𝜓 → 𝜑 )
3	0 2	wi	⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )