Theorem sbcco3g

Description: Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcco3gw when possible. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbcco3g.1	|- ( x = A -> B = C )
Assertion	sbcco3g	|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbcco3g.1	|- ( x = A -> B = C )
2		sbcnestg	|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
3		elex	|- ( A e. V -> A e. _V )
4		nfcvd	|- ( A e. _V -> F/_ x C )
5	4 1	csbiegf	|- ( A e. _V -> [_ A / x ]_ B = C )
6		dfsbcq	|- ( [_ A / x ]_ B = C -> ( [. [_ A / x ]_ B / y ]. ph <-> [. C / y ]. ph ) )
7	3 5 6	3syl	|- ( A e. V -> ( [. [_ A / x ]_ B / y ]. ph <-> [. C / y ]. ph ) )
8	2 7	bitrd	|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ph ) )