Theorem sbc3ie

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014) (Revised by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	sbc3ie.1	|- A e. _V
	sbc3ie.2	|- B e. _V
	sbc3ie.3	|- C e. _V
	sbc3ie.4	|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
Assertion	sbc3ie	|- ( [. A / x ]. [. B / y ]. [. C / z ]. ph <-> ps )

Proof

Step	Hyp	Ref	Expression
1		sbc3ie.1	|- A e. _V
2		sbc3ie.2	|- B e. _V
3		sbc3ie.3	|- C e. _V
4		sbc3ie.4	|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
5	3	a1i	|- ( ( x = A /\ y = B ) -> C e. _V )
6	4	3expa	|- ( ( ( x = A /\ y = B ) /\ z = C ) -> ( ph <-> ps ) )
7	5 6	sbcied	|- ( ( x = A /\ y = B ) -> ( [. C / z ]. ph <-> ps ) )
8	1 2 7	sbc2ie	|- ( [. A / x ]. [. B / y ]. [. C / z ]. ph <-> ps )