Metamath Proof Explorer


Theorem br6

Description: Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013) (Revised by Mario Carneiro, 3-May-2015)

Ref Expression
Hypotheses br6.1 a = A φ ψ
br6.2 b = B ψ χ
br6.3 c = C χ θ
br6.4 d = D θ τ
br6.5 e = E τ η
br6.6 f = F η ζ
br6.7 x = X P = Q
br6.8 R = p q | x S a P b P c P d P e P f P p = a b c q = d e f φ
Assertion br6 X S A Q B Q C Q D Q E Q F Q A B C R D E F ζ

Proof

Step Hyp Ref Expression
1 br6.1 a = A φ ψ
2 br6.2 b = B ψ χ
3 br6.3 c = C χ θ
4 br6.4 d = D θ τ
5 br6.5 e = E τ η
6 br6.6 f = F η ζ
7 br6.7 x = X P = Q
8 br6.8 R = p q | x S a P b P c P d P e P f P p = a b c q = d e f φ
9 opex A B C V
10 opex D E F V
11 eqeq1 p = A B C p = a b c A B C = a b c
12 eqcom A B C = a b c a b c = A B C
13 11 12 bitrdi p = A B C p = a b c a b c = A B C
14 13 3anbi1d p = A B C p = a b c q = d e f φ a b c = A B C q = d e f φ
15 14 rexbidv p = A B C f P p = a b c q = d e f φ f P a b c = A B C q = d e f φ
16 15 2rexbidv p = A B C d P e P f P p = a b c q = d e f φ d P e P f P a b c = A B C q = d e f φ
17 16 2rexbidv p = A B C b P c P d P e P f P p = a b c q = d e f φ b P c P d P e P f P a b c = A B C q = d e f φ
18 17 2rexbidv p = A B C x S a P b P c P d P e P f P p = a b c q = d e f φ x S a P b P c P d P e P f P a b c = A B C q = d e f φ
19 eqeq1 q = D E F q = d e f D E F = d e f
20 eqcom D E F = d e f d e f = D E F
21 19 20 bitrdi q = D E F q = d e f d e f = D E F
22 21 3anbi2d q = D E F a b c = A B C q = d e f φ a b c = A B C d e f = D E F φ
23 22 rexbidv q = D E F f P a b c = A B C q = d e f φ f P a b c = A B C d e f = D E F φ
24 23 2rexbidv q = D E F d P e P f P a b c = A B C q = d e f φ d P e P f P a b c = A B C d e f = D E F φ
25 24 2rexbidv q = D E F b P c P d P e P f P a b c = A B C q = d e f φ b P c P d P e P f P a b c = A B C d e f = D E F φ
26 25 2rexbidv q = D E F x S a P b P c P d P e P f P a b c = A B C q = d e f φ x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ
27 9 10 18 26 8 brab A B C R D E F x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ
28 vex a V
29 opex b c V
30 28 29 opth a b c = A B C a = A b c = B C
31 vex b V
32 vex c V
33 31 32 opth b c = B C b = B c = C
34 2 3 sylan9bb b = B c = C ψ θ
35 33 34 sylbi b c = B C ψ θ
36 1 35 sylan9bb a = A b c = B C φ θ
37 30 36 sylbi a b c = A B C φ θ
38 vex d V
39 opex e f V
40 38 39 opth d e f = D E F d = D e f = E F
41 vex e V
42 vex f V
43 41 42 opth e f = E F e = E f = F
44 5 6 sylan9bb e = E f = F τ ζ
45 43 44 sylbi e f = E F τ ζ
46 4 45 sylan9bb d = D e f = E F θ ζ
47 40 46 sylbi d e f = D E F θ ζ
48 37 47 sylan9bb a b c = A B C d e f = D E F φ ζ
49 48 biimp3a a b c = A B C d e f = D E F φ ζ
50 49 a1i X S A Q B Q C Q D Q E Q F Q x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ ζ
51 50 rexlimdva X S A Q B Q C Q D Q E Q F Q x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ ζ
52 51 rexlimdvva X S A Q B Q C Q D Q E Q F Q x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ ζ
53 52 rexlimdvva X S A Q B Q C Q D Q E Q F Q x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ ζ
54 53 rexlimdvva X S A Q B Q C Q D Q E Q F Q x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ ζ
55 simpl1 X S A Q B Q C Q D Q E Q F Q ζ X S
56 simpl2 X S A Q B Q C Q D Q E Q F Q ζ A Q B Q C Q
57 opeq1 d = D d e f = D e f
58 57 eqeq1d d = D d e f = D E F D e f = D E F
59 58 4 3anbi23d d = D A B C = A B C d e f = D E F θ A B C = A B C D e f = D E F τ
60 opeq1 e = E e f = E f
61 60 opeq2d e = E D e f = D E f
62 61 eqeq1d e = E D e f = D E F D E f = D E F
63 62 5 3anbi23d e = E A B C = A B C D e f = D E F τ A B C = A B C D E f = D E F η
64 opeq2 f = F E f = E F
65 64 opeq2d f = F D E f = D E F
66 65 eqeq1d f = F D E f = D E F D E F = D E F
67 66 6 3anbi23d f = F A B C = A B C D E f = D E F η A B C = A B C D E F = D E F ζ
68 eqid A B C = A B C
69 eqid D E F = D E F
70 68 69 pm3.2i A B C = A B C D E F = D E F
71 df-3an A B C = A B C D E F = D E F ζ A B C = A B C D E F = D E F ζ
72 70 71 mpbiran A B C = A B C D E F = D E F ζ ζ
73 67 72 bitrdi f = F A B C = A B C D E f = D E F η ζ
74 59 63 73 rspc3ev D Q E Q F Q ζ d Q e Q f Q A B C = A B C d e f = D E F θ
75 74 3ad2antl3 X S A Q B Q C Q D Q E Q F Q ζ d Q e Q f Q A B C = A B C d e f = D E F θ
76 opeq1 a = A a b c = A b c
77 76 eqeq1d a = A a b c = A B C A b c = A B C
78 77 1 3anbi13d a = A a b c = A B C d e f = D E F φ A b c = A B C d e f = D E F ψ
79 78 rexbidv a = A f Q a b c = A B C d e f = D E F φ f Q A b c = A B C d e f = D E F ψ
80 79 2rexbidv a = A d Q e Q f Q a b c = A B C d e f = D E F φ d Q e Q f Q A b c = A B C d e f = D E F ψ
81 opeq1 b = B b c = B c
82 81 opeq2d b = B A b c = A B c
83 82 eqeq1d b = B A b c = A B C A B c = A B C
84 83 2 3anbi13d b = B A b c = A B C d e f = D E F ψ A B c = A B C d e f = D E F χ
85 84 rexbidv b = B f Q A b c = A B C d e f = D E F ψ f Q A B c = A B C d e f = D E F χ
86 85 2rexbidv b = B d Q e Q f Q A b c = A B C d e f = D E F ψ d Q e Q f Q A B c = A B C d e f = D E F χ
87 opeq2 c = C B c = B C
88 87 opeq2d c = C A B c = A B C
89 88 eqeq1d c = C A B c = A B C A B C = A B C
90 89 3 3anbi13d c = C A B c = A B C d e f = D E F χ A B C = A B C d e f = D E F θ
91 90 rexbidv c = C f Q A B c = A B C d e f = D E F χ f Q A B C = A B C d e f = D E F θ
92 91 2rexbidv c = C d Q e Q f Q A B c = A B C d e f = D E F χ d Q e Q f Q A B C = A B C d e f = D E F θ
93 80 86 92 rspc3ev A Q B Q C Q d Q e Q f Q A B C = A B C d e f = D E F θ a Q b Q c Q d Q e Q f Q a b c = A B C d e f = D E F φ
94 56 75 93 syl2anc X S A Q B Q C Q D Q E Q F Q ζ a Q b Q c Q d Q e Q f Q a b c = A B C d e f = D E F φ
95 7 rexeqdv x = X f P a b c = A B C d e f = D E F φ f Q a b c = A B C d e f = D E F φ
96 7 95 rexeqbidv x = X e P f P a b c = A B C d e f = D E F φ e Q f Q a b c = A B C d e f = D E F φ
97 7 96 rexeqbidv x = X d P e P f P a b c = A B C d e f = D E F φ d Q e Q f Q a b c = A B C d e f = D E F φ
98 7 97 rexeqbidv x = X c P d P e P f P a b c = A B C d e f = D E F φ c Q d Q e Q f Q a b c = A B C d e f = D E F φ
99 7 98 rexeqbidv x = X b P c P d P e P f P a b c = A B C d e f = D E F φ b Q c Q d Q e Q f Q a b c = A B C d e f = D E F φ
100 7 99 rexeqbidv x = X a P b P c P d P e P f P a b c = A B C d e f = D E F φ a Q b Q c Q d Q e Q f Q a b c = A B C d e f = D E F φ
101 100 rspcev X S a Q b Q c Q d Q e Q f Q a b c = A B C d e f = D E F φ x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ
102 55 94 101 syl2anc X S A Q B Q C Q D Q E Q F Q ζ x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ
103 102 ex X S A Q B Q C Q D Q E Q F Q ζ x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ
104 54 103 impbid X S A Q B Q C Q D Q E Q F Q x S a P b P c P d P e P f P a b c = A B C d e f = D E F φ ζ
105 27 104 syl5bb X S A Q B Q C Q D Q E Q F Q A B C R D E F ζ