This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )