# 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 ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

### Proof

Step Hyp Ref Expression
1 sbccomlem ( [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐵 / 𝑤 ] [ 𝐴 / 𝑧 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
2 sbccomlem ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
3 2 sbcbii ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
4 sbccomlem ( [ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
5 3 4 bitri ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
6 5 sbcbii ( [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
7 sbccomlem ( [ 𝐴 / 𝑧 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
8 7 sbcbii ( [ 𝐵 / 𝑤 ] [ 𝐴 / 𝑧 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
9 1 6 8 3bitr3i ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
10 sbccow ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
11 sbccow ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐵 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
12 9 10 11 3bitr3i ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
13 sbccow ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] 𝜑 )
14 13 sbcbii ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
15 sbccow ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜑 )
16 15 sbcbii ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑[ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
17 12 14 16 3bitr3i ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )