Axiom ax-i5r 1549

Description: Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
ax-i5r	⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓))

Detailed syntax breakdown of Axiom ax-i5r

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vx	. . . 4 setvar 𝑥
3	1, 2	wal 1362	. . 3 wff ∀𝑥𝜑
4		wps	. . . 4 wff 𝜓
5	4, 2	wal 1362	. . 3 wff ∀𝑥𝜓
6	3, 5	wi 4	. 2 wff (∀𝑥𝜑 → ∀𝑥𝜓)
7	3, 4	wi 4	. . 3 wff (∀𝑥𝜑 → 𝜓)
8	7, 2	wal 1362	. 2 wff ∀𝑥(∀𝑥𝜑 → 𝜓)
9	6, 8	wi 4	1 wff ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓))

This axiom is referenced by:  hbim  1559  hbimd  1587