Theorem sbccom2fi

Description: Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		sbccom2fi.1	|- A e. _V
2		sbccom2fi.2	|- F/_ y A
3		sbccom2fi.3	|- [_ A / x ]_ B = C
4		sbccom2fi.4	|- ( [. A / x ]. ph <-> ps )
5	1 2	sbccom2f	|- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
6		dfsbcq	|- ( [_ A / x ]_ B = C -> ( [. [_ A / x ]_ B / y ]. [. A / x ]. ph <-> [. C / y ]. [. A / x ]. ph ) )
7	3 6	ax-mp	|- ( [. [_ A / x ]_ B / y ]. [. A / x ]. ph <-> [. C / y ]. [. A / x ]. ph )
8	4	sbcbii	|- ( [. C / y ]. [. A / x ]. ph <-> [. C / y ]. ps )
9	5 7 8	3bitri	|- ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ps )