Axiom ax-frege1 38084

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 6. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-frege1	|- ( ph -> ( ps -> ph ) )

Detailed syntax breakdown of Axiom ax-frege1

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		wps	. . 3 wff ps
3	2, 1	wi 4	. 2 wff ( ps -> ph )
4	1, 3	wi 4	1 wff ( ph -> ( ps -> ph ) )

This axiom is referenced by:  rp-simp2-frege  38086  rp-frege3g  38088  frege3  38089  frege5  38094  rp-6frege  38097  frege26  38104  frege27  38105  frege11  38108  frege24  38109  frege36  38133