Axiom ax-i5r 1528

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

Assertion

Ref	Expression
ax-i5r	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )

Detailed syntax breakdown of Axiom ax-i5r

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff ph
2		vx	. . . 4 setvar x
3	1, 2	wal 1346	. . 3 wff A. x ph
4		wps	. . . 4 wff ps
5	4, 2	wal 1346	. . 3 wff A. x ps
6	3, 5	wi 4	. 2 wff ( A. x ph -> A. x ps )
7	3, 4	wi 4	. . 3 wff ( A. x ph -> ps )
8	7, 2	wal 1346	. 2 wff A. x ( A. x ph -> ps )
9	6, 8	wi 4	1 wff ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )

This axiom is referenced by:  hbim  1538  hbimd  1566