Theorem sbccom

Description: Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005) (Proof shortened by Mario Carneiro, 18-Oct-2016)

	Ref	Expression
Assertion	sbccom	|- ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbccomlem	|- ( [. A / z ]. [. B / w ]. [. w / y ]. [. z / x ]. ph <-> [. B / w ]. [. A / z ]. [. w / y ]. [. z / x ]. ph )
2		sbccomlem	|- ( [. w / y ]. [. z / x ]. ph <-> [. z / x ]. [. w / y ]. ph )
3	2	sbcbii	|- ( [. B / w ]. [. w / y ]. [. z / x ]. ph <-> [. B / w ]. [. z / x ]. [. w / y ]. ph )
4		sbccomlem	|- ( [. B / w ]. [. z / x ]. [. w / y ]. ph <-> [. z / x ]. [. B / w ]. [. w / y ]. ph )
5	3 4	bitri	|- ( [. B / w ]. [. w / y ]. [. z / x ]. ph <-> [. z / x ]. [. B / w ]. [. w / y ]. ph )
6	5	sbcbii	|- ( [. A / z ]. [. B / w ]. [. w / y ]. [. z / x ]. ph <-> [. A / z ]. [. z / x ]. [. B / w ]. [. w / y ]. ph )
7		sbccomlem	|- ( [. A / z ]. [. w / y ]. [. z / x ]. ph <-> [. w / y ]. [. A / z ]. [. z / x ]. ph )
8	7	sbcbii	|- ( [. B / w ]. [. A / z ]. [. w / y ]. [. z / x ]. ph <-> [. B / w ]. [. w / y ]. [. A / z ]. [. z / x ]. ph )
9	1 6 8	3bitr3i	|- ( [. A / z ]. [. z / x ]. [. B / w ]. [. w / y ]. ph <-> [. B / w ]. [. w / y ]. [. A / z ]. [. z / x ]. ph )
10		sbccow	|- ( [. A / z ]. [. z / x ]. [. B / w ]. [. w / y ]. ph <-> [. A / x ]. [. B / w ]. [. w / y ]. ph )
11		sbccow	|- ( [. B / w ]. [. w / y ]. [. A / z ]. [. z / x ]. ph <-> [. B / y ]. [. A / z ]. [. z / x ]. ph )
12	9 10 11	3bitr3i	|- ( [. A / x ]. [. B / w ]. [. w / y ]. ph <-> [. B / y ]. [. A / z ]. [. z / x ]. ph )
13		sbccow	|- ( [. B / w ]. [. w / y ]. ph <-> [. B / y ]. ph )
14	13	sbcbii	|- ( [. A / x ]. [. B / w ]. [. w / y ]. ph <-> [. A / x ]. [. B / y ]. ph )
15		sbccow	|- ( [. A / z ]. [. z / x ]. ph <-> [. A / x ]. ph )
16	15	sbcbii	|- ( [. B / y ]. [. A / z ]. [. z / x ]. ph <-> [. B / y ]. [. A / x ]. ph )
17	12 14 16	3bitr3i	|- ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph )