Metamath Proof Explorer


Theorem br8d

Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013) (Revised by Mario Carneiro, 3-May-2015) (Revised by Thierry Arnoux, 21-Mar-2019)

Ref Expression
Hypotheses br8d.1 a = A ψ χ
br8d.2 b = B χ θ
br8d.3 c = C θ τ
br8d.4 d = D τ η
br8d.5 e = E η ζ
br8d.6 f = F ζ σ
br8d.7 g = G σ ρ
br8d.8 h = H ρ μ
br8d.10 φ R = p q | a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ
br8d.11 φ A P
br8d.12 φ B P
br8d.13 φ C P
br8d.14 φ D P
br8d.15 φ E P
br8d.16 φ F P
br8d.17 φ G P
br8d.18 φ H P
Assertion br8d φ A B C D R E F G H μ

Proof

Step Hyp Ref Expression
1 br8d.1 a = A ψ χ
2 br8d.2 b = B χ θ
3 br8d.3 c = C θ τ
4 br8d.4 d = D τ η
5 br8d.5 e = E η ζ
6 br8d.6 f = F ζ σ
7 br8d.7 g = G σ ρ
8 br8d.8 h = H ρ μ
9 br8d.10 φ R = p q | a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ
10 br8d.11 φ A P
11 br8d.12 φ B P
12 br8d.13 φ C P
13 br8d.14 φ D P
14 br8d.15 φ E P
15 br8d.16 φ F P
16 br8d.17 φ G P
17 br8d.18 φ H P
18 9 breqd φ A B C D R E F G H A B C D p q | a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ E F G H
19 opex A B C D V
20 opex E F G H V
21 eqeq1 p = A B C D p = a b c d A B C D = a b c d
22 21 3anbi1d p = A B C D p = a b c d q = e f g h ψ A B C D = a b c d q = e f g h ψ
23 22 rexbidv p = A B C D h P p = a b c d q = e f g h ψ h P A B C D = a b c d q = e f g h ψ
24 23 2rexbidv p = A B C D f P g P h P p = a b c d q = e f g h ψ f P g P h P A B C D = a b c d q = e f g h ψ
25 24 2rexbidv p = A B C D d P e P f P g P h P p = a b c d q = e f g h ψ d P e P f P g P h P A B C D = a b c d q = e f g h ψ
26 25 2rexbidv p = A B C D b P c P d P e P f P g P h P p = a b c d q = e f g h ψ b P c P d P e P f P g P h P A B C D = a b c d q = e f g h ψ
27 26 rexbidv p = A B C D a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ a P b P c P d P e P f P g P h P A B C D = a b c d q = e f g h ψ
28 eqeq1 q = E F G H q = e f g h E F G H = e f g h
29 28 3anbi2d q = E F G H A B C D = a b c d q = e f g h ψ A B C D = a b c d E F G H = e f g h ψ
30 29 rexbidv q = E F G H h P A B C D = a b c d q = e f g h ψ h P A B C D = a b c d E F G H = e f g h ψ
31 30 2rexbidv q = E F G H f P g P h P A B C D = a b c d q = e f g h ψ f P g P h P A B C D = a b c d E F G H = e f g h ψ
32 31 2rexbidv q = E F G H d P e P f P g P h P A B C D = a b c d q = e f g h ψ d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
33 32 2rexbidv q = E F G H b P c P d P e P f P g P h P A B C D = a b c d q = e f g h ψ b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
34 33 rexbidv q = E F G H a P b P c P d P e P f P g P h P A B C D = a b c d q = e f g h ψ a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
35 eqid p q | a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ = p q | a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ
36 19 20 27 34 35 brab A B C D p q | a P b P c P d P e P f P g P h P p = a b c d q = e f g h ψ E F G H a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
37 18 36 bitrdi φ A B C D R E F G H a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
38 opex a b V
39 opex c d V
40 38 39 opth a b c d = A B C D a b = A B c d = C D
41 vex a V
42 vex b V
43 41 42 opth a b = A B a = A b = B
44 1 2 sylan9bb a = A b = B ψ θ
45 43 44 sylbi a b = A B ψ θ
46 vex c V
47 vex d V
48 46 47 opth c d = C D c = C d = D
49 3 4 sylan9bb c = C d = D θ η
50 48 49 sylbi c d = C D θ η
51 45 50 sylan9bb a b = A B c d = C D ψ η
52 40 51 sylbi a b c d = A B C D ψ η
53 52 eqcoms A B C D = a b c d ψ η
54 opex e f V
55 opex g h V
56 54 55 opth e f g h = E F G H e f = E F g h = G H
57 vex e V
58 vex f V
59 57 58 opth e f = E F e = E f = F
60 5 6 sylan9bb e = E f = F η σ
61 59 60 sylbi e f = E F η σ
62 vex g V
63 vex h V
64 62 63 opth g h = G H g = G h = H
65 7 8 sylan9bb g = G h = H σ μ
66 64 65 sylbi g h = G H σ μ
67 61 66 sylan9bb e f = E F g h = G H η μ
68 56 67 sylbi e f g h = E F G H η μ
69 68 eqcoms E F G H = e f g h η μ
70 53 69 sylan9bb A B C D = a b c d E F G H = e f g h ψ μ
71 70 biimp3a A B C D = a b c d E F G H = e f g h ψ μ
72 71 a1i A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
73 72 rexlimdva A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
74 73 rexlimdvva A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
75 74 rexlimdvva A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
76 75 rexlimdvva A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
77 76 rexlimdva A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
78 simpl1l A P B P C P D P E P F P G P H P μ A P
79 simpl1r A P B P C P D P E P F P G P H P μ B P
80 simpl21 A P B P C P D P E P F P G P H P μ C P
81 simpl22 A P B P C P D P E P F P G P H P μ D P
82 simpl23 A P B P C P D P E P F P G P H P μ E P
83 simpl31 A P B P C P D P E P F P G P H P μ F P
84 simpl32 A P B P C P D P E P F P G P H P μ G P
85 simpl33 A P B P C P D P E P F P G P H P μ H P
86 eqidd A P B P C P D P E P F P G P H P μ A B C D = A B C D
87 eqidd A P B P C P D P E P F P G P H P μ E F G H = E F G H
88 simpr A P B P C P D P E P F P G P H P μ μ
89 opeq1 g = G g h = G h
90 89 opeq2d g = G E F g h = E F G h
91 90 eqeq2d g = G E F G H = E F g h E F G H = E F G h
92 91 7 3anbi23d g = G A B C D = A B C D E F G H = E F g h σ A B C D = A B C D E F G H = E F G h ρ
93 opeq2 h = H G h = G H
94 93 opeq2d h = H E F G h = E F G H
95 94 eqeq2d h = H E F G H = E F G h E F G H = E F G H
96 95 8 3anbi23d h = H A B C D = A B C D E F G H = E F G h ρ A B C D = A B C D E F G H = E F G H μ
97 92 96 rspc2ev G P H P A B C D = A B C D E F G H = E F G H μ g P h P A B C D = A B C D E F G H = E F g h σ
98 84 85 86 87 88 97 syl113anc A P B P C P D P E P F P G P H P μ g P h P A B C D = A B C D E F G H = E F g h σ
99 opeq2 d = D C d = C D
100 99 opeq2d d = D A B C d = A B C D
101 100 eqeq2d d = D A B C D = A B C d A B C D = A B C D
102 101 4 3anbi13d d = D A B C D = A B C d E F G H = e f g h τ A B C D = A B C D E F G H = e f g h η
103 102 2rexbidv d = D g P h P A B C D = A B C d E F G H = e f g h τ g P h P A B C D = A B C D E F G H = e f g h η
104 opeq1 e = E e f = E f
105 104 opeq1d e = E e f g h = E f g h
106 105 eqeq2d e = E E F G H = e f g h E F G H = E f g h
107 106 5 3anbi23d e = E A B C D = A B C D E F G H = e f g h η A B C D = A B C D E F G H = E f g h ζ
108 107 2rexbidv e = E g P h P A B C D = A B C D E F G H = e f g h η g P h P A B C D = A B C D E F G H = E f g h ζ
109 opeq2 f = F E f = E F
110 109 opeq1d f = F E f g h = E F g h
111 110 eqeq2d f = F E F G H = E f g h E F G H = E F g h
112 111 6 3anbi23d f = F A B C D = A B C D E F G H = E f g h ζ A B C D = A B C D E F G H = E F g h σ
113 112 2rexbidv f = F g P h P A B C D = A B C D E F G H = E f g h ζ g P h P A B C D = A B C D E F G H = E F g h σ
114 103 108 113 rspc3ev D P E P F P g P h P A B C D = A B C D E F G H = E F g h σ d P e P f P g P h P A B C D = A B C d E F G H = e f g h τ
115 81 82 83 98 114 syl31anc A P B P C P D P E P F P G P H P μ d P e P f P g P h P A B C D = A B C d E F G H = e f g h τ
116 opeq1 a = A a b = A b
117 116 opeq1d a = A a b c d = A b c d
118 117 eqeq2d a = A A B C D = a b c d A B C D = A b c d
119 118 1 3anbi13d a = A A B C D = a b c d E F G H = e f g h ψ A B C D = A b c d E F G H = e f g h χ
120 119 rexbidv a = A h P A B C D = a b c d E F G H = e f g h ψ h P A B C D = A b c d E F G H = e f g h χ
121 120 2rexbidv a = A f P g P h P A B C D = a b c d E F G H = e f g h ψ f P g P h P A B C D = A b c d E F G H = e f g h χ
122 121 2rexbidv a = A d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ d P e P f P g P h P A B C D = A b c d E F G H = e f g h χ
123 opeq2 b = B A b = A B
124 123 opeq1d b = B A b c d = A B c d
125 124 eqeq2d b = B A B C D = A b c d A B C D = A B c d
126 125 2 3anbi13d b = B A B C D = A b c d E F G H = e f g h χ A B C D = A B c d E F G H = e f g h θ
127 126 rexbidv b = B h P A B C D = A b c d E F G H = e f g h χ h P A B C D = A B c d E F G H = e f g h θ
128 127 2rexbidv b = B f P g P h P A B C D = A b c d E F G H = e f g h χ f P g P h P A B C D = A B c d E F G H = e f g h θ
129 128 2rexbidv b = B d P e P f P g P h P A B C D = A b c d E F G H = e f g h χ d P e P f P g P h P A B C D = A B c d E F G H = e f g h θ
130 opeq1 c = C c d = C d
131 130 opeq2d c = C A B c d = A B C d
132 131 eqeq2d c = C A B C D = A B c d A B C D = A B C d
133 132 3 3anbi13d c = C A B C D = A B c d E F G H = e f g h θ A B C D = A B C d E F G H = e f g h τ
134 133 rexbidv c = C h P A B C D = A B c d E F G H = e f g h θ h P A B C D = A B C d E F G H = e f g h τ
135 134 2rexbidv c = C f P g P h P A B C D = A B c d E F G H = e f g h θ f P g P h P A B C D = A B C d E F G H = e f g h τ
136 135 2rexbidv c = C d P e P f P g P h P A B C D = A B c d E F G H = e f g h θ d P e P f P g P h P A B C D = A B C d E F G H = e f g h τ
137 122 129 136 rspc3ev A P B P C P d P e P f P g P h P A B C D = A B C d E F G H = e f g h τ a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
138 78 79 80 115 137 syl31anc A P B P C P D P E P F P G P H P μ a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
139 138 ex A P B P C P D P E P F P G P H P μ a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ
140 77 139 impbid A P B P C P D P E P F P G P H P a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
141 10 11 12 13 14 15 16 17 140 syl233anc φ a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h ψ μ
142 37 141 bitrd φ A B C D R E F G H μ