Axiom ax-eac1 33

Description: & elimination rule, left hand side.

Hypothesis

Ref	Expression
ax-eac1.1	⊦ (~ 𝜑 ⅋ (𝜓 & 𝜒))

Assertion

Ref	Expression
ax-eac1	⊦ (~ 𝜑 ⅋ 𝜓)

Detailed syntax breakdown of Axiom ax-eac1

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wneg 3	. 2 wff ~ 𝜑
3		wps	. 2 wff 𝜓
4	2, 3	wmd 2	1 wff (~ 𝜑 ⅋ 𝜓)

This axiom is referenced by:  eac1d  37  eac1i  38  lbi1s  87  lbsymd  102  abs1  178