Axiom ax-dig 54

Description: If all the elements of a multiplicative disjunction have ?, then ? can be removed from that disjunction.

Assertion

Ref	Expression
ax-dig	⊦ (~ ? (? 𝜑 ⅋ ? 𝜓) ⅋ (? 𝜑 ⅋ ? 𝜓))

Detailed syntax breakdown of Axiom ax-dig

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff 𝜑
2	1	wne 48	. . . . 5 wff ? 𝜑
3		wps	. . . . . 6 wff 𝜓
4	3	wne 48	. . . . 5 wff ? 𝜓
5	2, 4	wmd 2	. . . 4 wff (? 𝜑 ⅋ ? 𝜓)
6	5	wne 48	. . 3 wff ? (? 𝜑 ⅋ ? 𝜓)
7	6	wneg 3	. 2 wff ~ ? (? 𝜑 ⅋ ? 𝜓)
8	7, 5	wmd 2	1 wff (~ ? (? 𝜑 ⅋ ? 𝜓) ⅋ (? 𝜑 ⅋ ? 𝜓))

This axiom is referenced by: (None)