Axiom ax-almd 324

Description: Quantified multiplicative disjunction. This "distributes" a quantifier over linear implication.

Assertion

Ref	Expression
ax-almd	⊦ (∀x(𝜑 ⊸ 𝜓) ⊸ (∀x𝜑 ⊸ ∀x𝜓))

Detailed syntax breakdown of Axiom ax-almd

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		wps	. . . 4 wff 𝜓
3	1, 2	wli 61	. . 3 wff (𝜑 ⊸ 𝜓)
4		vx	. . 3 var x
5	3, 4	wal 318	. 2 wff ∀x(𝜑 ⊸ 𝜓)
6	1, 4	wal 318	. . 3 wff ∀x𝜑
7	2, 4	wal 318	. . 3 wff ∀x𝜓
8	6, 7	wli 61	. 2 wff (∀x𝜑 ⊸ ∀x𝜓)
9	5, 8	wli 61	1 wff (∀x(𝜑 ⊸ 𝜓) ⊸ (∀x𝜑 ⊸ ∀x𝜓))

This axiom is referenced by: (None)