Axiom ax-frege1

Description: The case in which ph is denied, ps is affirmed, and ph is affirmed is excluded. This is evident since ph cannot at the same time be denied and affirmed. Axiom 1 of Frege1879 p. 26. Identical to ax-1 . (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-frege1	$$⊢\phi \to \left(\psi \to \phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	1 0	wi	$$wff\left(\psi \to \phi \right)$$
3	0 2	wi	$$wff\left(\phi \to \left(\psi \to \phi \right)\right)$$