Axiom ax-iac 32

Description: & introduction rule.

Hypotheses

Ref	Expression
ax-iac.1	⊦ (~ 𝜑 ⅋ 𝜓)
ax-iac.2	⊦ (~ 𝜑 ⅋ 𝜒)

Assertion

Ref	Expression
ax-iac	⊦ (~ 𝜑 ⅋ (𝜓 & 𝜒))

Detailed syntax breakdown of Axiom ax-iac

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wneg 3	. 2 wff ~ 𝜑
3		wps	. . 3 wff 𝜓
4		wch	. . 3 wff 𝜒
5	3, 4	wac 30	. 2 wff (𝜓 & 𝜒)
6	2, 5	wmd 2	1 wff (~ 𝜑 ⅋ (𝜓 & 𝜒))

This axiom is referenced by:  iac  35  itopi  41  dflb1s  91  ilbd  97  abs1  178