Theorem br8d 27601

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.)

Hypotheses

Ref	Expression
br8d.1	|- ( a = A -> ( ps <-> ch ) )
br8d.2	|- ( b = B -> ( ch <-> th ) )
br8d.3	|- ( c = C -> ( th <-> ta ) )
br8d.4	|- ( d = D -> ( ta <-> et ) )
br8d.5	|- ( e = E -> ( et <-> ze ) )
br8d.6	|- ( f = F -> ( ze <-> si ) )
br8d.7	|- ( g = G -> ( si <-> rh ) )
br8d.8	|- ( h = H -> ( rh <-> mu ) )
br8d.10	|- ( ph -> R = { <. p , q >. | E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) } )
br8d.11	|- ( ph -> A e. P )
br8d.12	|- ( ph -> B e. P )
br8d.13	|- ( ph -> C e. P )
br8d.14	|- ( ph -> D e. P )
br8d.15	|- ( ph -> E e. P )
br8d.16	|- ( ph -> F e. P )
br8d.17	|- ( ph -> G e. P )
br8d.18	|- ( ph -> H e. P )

Assertion

Ref	Expression
br8d	|- ( ph -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> mu ) )

Distinct variable groups:   a, b, c, d, e, f, g, h, p, q, A   B, a, b, c, d, e, f, g, h, p, q   C, a, b, c, d, e, f, g, h, p, q   D, a, b, c, d, e, f, g, h, p, q   E, a, b, c, d, e, f, g, h, p, q   F, a, b, c, d, e, f, g, h, p, q   G, a, b, c, d, e, f, g, h, p, q   H, a, b, c, d, e, f, g, h, p, q   P, a, b, c, d, e, f, g, h, p, q   ch, a   th, b   ta, c   et, d   ze, e   si, f   rh, g   ps, p, q   mu, a, b, c, d, e, f, g, h

Allowed substitution hints:   ph( e, f, g, h, q, p, a, b, c, d)   ps( e, f, g, h, a, b, c, d)   ch( e, f, g, h, q, p, b, c, d)   th( e, f, g, h, q, p, a, c, d)   ta( e, f, g, h, q, p, a, b, d)   et( e, f, g, h, q, p, a, b, c)   ze( f, g, h, q, p, a, b, c, d)   si( e, g, h, q, p, a, b, c, d)   rh( e, f, h, q, p, a, b, c, d)   mu( q, p)   R( e, f, g, h, q, p, a, b, c, d)

Proof of Theorem br8d

Step	Hyp	Ref	Expression
1		br8d.10	. . . 4 |- ( ph -> R = { <. p , q >. | E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) } )
2	1	breqd 4467	. . 3 |- ( ph -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> <. <. A , B >. , <. C , D >. >. { <. p , q >. | E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) } <. <. E , F >. , <. G , H >. >. ) )
3		opex 4720	. . . 4 |- <. <. A , B >. , <. C , D >. >. e. _V
4		opex 4720	. . . 4 |- <. <. E , F >. , <. G , H >. >. e. _V
5		eqeq1 2461	. . . . . . . . . 10 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( p = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. ) )
6	5	3anbi1d 1303	. . . . . . . . 9 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
7	6	rexbidv 2968	. . . . . . . 8 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
8	7	2rexbidv 2975	. . . . . . 7 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
9	8	2rexbidv 2975	. . . . . 6 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
10	9	2rexbidv 2975	. . . . 5 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
11	10	rexbidv 2968	. . . 4 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
12		eqeq1 2461	. . . . . . . . . 10 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( q = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) )
13	12	3anbi2d 1304	. . . . . . . . 9 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
14	13	rexbidv 2968	. . . . . . . 8 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
15	14	2rexbidv 2975	. . . . . . 7 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
16	15	2rexbidv 2975	. . . . . 6 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
17	16	2rexbidv 2975	. . . . 5 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
18	17	rexbidv 2968	. . . 4 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
19		eqid 2457	. . . 4 |- { <. p , q >. | E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) } = { <. p , q >. | E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) }
20	3, 4, 11, 18, 19	brab 4779	. . 3 |- ( <. <. A , B >. , <. C , D >. >. { <. p , q >. | E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ps ) } <. <. E , F >. , <. G , H >. >. <-> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) )
21	2, 20	syl6bb 261	. 2 |- ( ph -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
22		br8d.11	. . 3 |- ( ph -> A e. P )
23		br8d.12	. . 3 |- ( ph -> B e. P )
24		br8d.13	. . 3 |- ( ph -> C e. P )
25		br8d.14	. . 3 |- ( ph -> D e. P )
26		br8d.15	. . 3 |- ( ph -> E e. P )
27		br8d.16	. . 3 |- ( ph -> F e. P )
28		br8d.17	. . 3 |- ( ph -> G e. P )
29		br8d.18	. . 3 |- ( ph -> H e. P )
30		opex 4720	. . . . . . . . . . . . . . 15 |- <. a , b >. e. _V
31		opex 4720	. . . . . . . . . . . . . . 15 |- <. c , d >. e. _V
32	30, 31	opth 4730	. . . . . . . . . . . . . 14 |- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) )
33		vex 3112	. . . . . . . . . . . . . . . . 17 |- a e. _V
34		vex 3112	. . . . . . . . . . . . . . . . 17 |- b e. _V
35	33, 34	opth 4730	. . . . . . . . . . . . . . . 16 |- ( <. a , b >. = <. A , B >. <-> ( a = A /\ b = B ) )
36		br8d.1	. . . . . . . . . . . . . . . . 17 |- ( a = A -> ( ps <-> ch ) )
37		br8d.2	. . . . . . . . . . . . . . . . 17 |- ( b = B -> ( ch <-> th ) )
38	36, 37	sylan9bb 699	. . . . . . . . . . . . . . . 16 |- ( ( a = A /\ b = B ) -> ( ps <-> th ) )
39	35, 38	sylbi 195	. . . . . . . . . . . . . . 15 |- ( <. a , b >. = <. A , B >. -> ( ps <-> th ) )
40		vex 3112	. . . . . . . . . . . . . . . . 17 |- c e. _V
41		vex 3112	. . . . . . . . . . . . . . . . 17 |- d e. _V
42	40, 41	opth 4730	. . . . . . . . . . . . . . . 16 |- ( <. c , d >. = <. C , D >. <-> ( c = C /\ d = D ) )
43		br8d.3	. . . . . . . . . . . . . . . . 17 |- ( c = C -> ( th <-> ta ) )
44		br8d.4	. . . . . . . . . . . . . . . . 17 |- ( d = D -> ( ta <-> et ) )
45	43, 44	sylan9bb 699	. . . . . . . . . . . . . . . 16 |- ( ( c = C /\ d = D ) -> ( th <-> et ) )
46	42, 45	sylbi 195	. . . . . . . . . . . . . . 15 |- ( <. c , d >. = <. C , D >. -> ( th <-> et ) )
47	39, 46	sylan9bb 699	. . . . . . . . . . . . . 14 |- ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) -> ( ps <-> et ) )
48	32, 47	sylbi 195	. . . . . . . . . . . . 13 |- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. -> ( ps <-> et ) )
49	48	eqcoms 2469	. . . . . . . . . . . 12 |- ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. -> ( ps <-> et ) )
50		opex 4720	. . . . . . . . . . . . . . 15 |- <. e , f >. e. _V
51		opex 4720	. . . . . . . . . . . . . . 15 |- <. g , h >. e. _V
52	50, 51	opth 4730	. . . . . . . . . . . . . 14 |- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. <-> ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) )
53		vex 3112	. . . . . . . . . . . . . . . . 17 |- e e. _V
54		vex 3112	. . . . . . . . . . . . . . . . 17 |- f e. _V
55	53, 54	opth 4730	. . . . . . . . . . . . . . . 16 |- ( <. e , f >. = <. E , F >. <-> ( e = E /\ f = F ) )
56		br8d.5	. . . . . . . . . . . . . . . . 17 |- ( e = E -> ( et <-> ze ) )
57		br8d.6	. . . . . . . . . . . . . . . . 17 |- ( f = F -> ( ze <-> si ) )
58	56, 57	sylan9bb 699	. . . . . . . . . . . . . . . 16 |- ( ( e = E /\ f = F ) -> ( et <-> si ) )
59	55, 58	sylbi 195	. . . . . . . . . . . . . . 15 |- ( <. e , f >. = <. E , F >. -> ( et <-> si ) )
60		vex 3112	. . . . . . . . . . . . . . . . 17 |- g e. _V
61		vex 3112	. . . . . . . . . . . . . . . . 17 |- h e. _V
62	60, 61	opth 4730	. . . . . . . . . . . . . . . 16 |- ( <. g , h >. = <. G , H >. <-> ( g = G /\ h = H ) )
63		br8d.7	. . . . . . . . . . . . . . . . 17 |- ( g = G -> ( si <-> rh ) )
64		br8d.8	. . . . . . . . . . . . . . . . 17 |- ( h = H -> ( rh <-> mu ) )
65	63, 64	sylan9bb 699	. . . . . . . . . . . . . . . 16 |- ( ( g = G /\ h = H ) -> ( si <-> mu ) )
66	62, 65	sylbi 195	. . . . . . . . . . . . . . 15 |- ( <. g , h >. = <. G , H >. -> ( si <-> mu ) )
67	59, 66	sylan9bb 699	. . . . . . . . . . . . . 14 |- ( ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) -> ( et <-> mu ) )
68	52, 67	sylbi 195	. . . . . . . . . . . . 13 |- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. -> ( et <-> mu ) )
69	68	eqcoms 2469	. . . . . . . . . . . 12 |- ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. -> ( et <-> mu ) )
70	49, 69	sylan9bb 699	. . . . . . . . . . 11 |- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) -> ( ps <-> mu ) )
71	70	biimp3a 1328	. . . . . . . . . 10 |- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu )
72	71	a1i 11	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ a e. P ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) /\ ( f e. P /\ g e. P ) ) /\ h e. P ) -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu ) )
73	72	rexlimdva 2949	. . . . . . . 8 |- ( ( ( ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ a e. P ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) /\ ( f e. P /\ g e. P ) ) -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu ) )
74	73	rexlimdvva 2956	. . . . . . 7 |- ( ( ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ a e. P ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu ) )
75	74	rexlimdvva 2956	. . . . . 6 |- ( ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ a e. P ) /\ ( b e. P /\ c e. P ) ) -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu ) )
76	75	rexlimdvva 2956	. . . . 5 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ a e. P ) -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu ) )
77	76	rexlimdva 2949	. . . 4 |- ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) -> mu ) )
78		simpl1l 1047	. . . . . 6 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> A e. P )
79		simpl1r 1048	. . . . . 6 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> B e. P )
80		simpl21 1074	. . . . . 6 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> C e. P )
81		simpl22 1075	. . . . . . 7 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> D e. P )
82		simpl23 1076	. . . . . . 7 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> E e. P )
83		simpl31 1077	. . . . . . 7 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> F e. P )
84		simpl32 1078	. . . . . . . 8 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> G e. P )
85		simpl33 1079	. . . . . . . 8 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> H e. P )
86		eqidd 2458	. . . . . . . 8 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. )
87		eqidd 2458	. . . . . . . 8 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. )
88		simpr 461	. . . . . . . 8 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> mu )
89		opeq1 4219	. . . . . . . . . . . 12 |- ( g = G -> <. g , h >. = <. G , h >. )
90	89	opeq2d 4226	. . . . . . . . . . 11 |- ( g = G -> <. <. E , F >. , <. g , h >. >. = <. <. E , F >. , <. G , h >. >. )
91	90	eqeq2d 2471	. . . . . . . . . 10 |- ( g = G -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. ) )
92	91, 63	3anbi23d 1302	. . . . . . . . 9 |- ( g = G -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ si ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. /\ rh ) ) )
93		opeq2 4220	. . . . . . . . . . . 12 |- ( h = H -> <. G , h >. = <. G , H >. )
94	93	opeq2d 4226	. . . . . . . . . . 11 |- ( h = H -> <. <. E , F >. , <. G , h >. >. = <. <. E , F >. , <. G , H >. >. )
95	94	eqeq2d 2471	. . . . . . . . . 10 |- ( h = H -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. ) )
96	95, 64	3anbi23d 1302	. . . . . . . . 9 |- ( h = H -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. /\ rh ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. /\ mu ) ) )
97	92, 96	rspc2ev 3221	. . . . . . . 8 |- ( ( G e. P /\ H e. P /\ ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. /\ mu ) ) -> E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ si ) )
98	84, 85, 86, 87, 88, 97	syl113anc 1240	. . . . . . 7 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ si ) )
99		opeq2 4220	. . . . . . . . . . . 12 |- ( d = D -> <. C , d >. = <. C , D >. )
100	99	opeq2d 4226	. . . . . . . . . . 11 |- ( d = D -> <. <. A , B >. , <. C , d >. >. = <. <. A , B >. , <. C , D >. >. )
101	100	eqeq2d 2471	. . . . . . . . . 10 |- ( d = D -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. ) )
102	101, 44	3anbi13d 1301	. . . . . . . . 9 |- ( d = D -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ et ) ) )
103	102	2rexbidv 2975	. . . . . . . 8 |- ( d = D -> ( E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) <-> E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ et ) ) )
104		opeq1 4219	. . . . . . . . . . . 12 |- ( e = E -> <. e , f >. = <. E , f >. )
105	104	opeq1d 4225	. . . . . . . . . . 11 |- ( e = E -> <. <. e , f >. , <. g , h >. >. = <. <. E , f >. , <. g , h >. >. )
106	105	eqeq2d 2471	. . . . . . . . . 10 |- ( e = E -> ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. ) )
107	106, 56	3anbi23d 1302	. . . . . . . . 9 |- ( e = E -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ et ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ ze ) ) )
108	107	2rexbidv 2975	. . . . . . . 8 |- ( e = E -> ( E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ et ) <-> E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ ze ) ) )
109		opeq2 4220	. . . . . . . . . . . 12 |- ( f = F -> <. E , f >. = <. E , F >. )
110	109	opeq1d 4225	. . . . . . . . . . 11 |- ( f = F -> <. <. E , f >. , <. g , h >. >. = <. <. E , F >. , <. g , h >. >. )
111	110	eqeq2d 2471	. . . . . . . . . 10 |- ( f = F -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. ) )
112	111, 57	3anbi23d 1302	. . . . . . . . 9 |- ( f = F -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ ze ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ si ) ) )
113	112	2rexbidv 2975	. . . . . . . 8 |- ( f = F -> ( E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ ze ) <-> E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ si ) ) )
114	103, 108, 113	rspc3ev 3223	. . . . . . 7 |- ( ( ( D e. P /\ E e. P /\ F e. P ) /\ E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ si ) ) -> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) )
115	81, 82, 83, 98, 114	syl31anc 1231	. . . . . 6 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) )
116		opeq1 4219	. . . . . . . . . . . . 13 |- ( a = A -> <. a , b >. = <. A , b >. )
117	116	opeq1d 4225	. . . . . . . . . . . 12 |- ( a = A -> <. <. a , b >. , <. c , d >. >. = <. <. A , b >. , <. c , d >. >. )
118	117	eqeq2d 2471	. . . . . . . . . . 11 |- ( a = A -> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. ) )
119	118, 36	3anbi13d 1301	. . . . . . . . . 10 |- ( a = A -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
120	119	rexbidv 2968	. . . . . . . . 9 |- ( a = A -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
121	120	2rexbidv 2975	. . . . . . . 8 |- ( a = A -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
122	121	2rexbidv 2975	. . . . . . 7 |- ( a = A -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
123		opeq2 4220	. . . . . . . . . . . . 13 |- ( b = B -> <. A , b >. = <. A , B >. )
124	123	opeq1d 4225	. . . . . . . . . . . 12 |- ( b = B -> <. <. A , b >. , <. c , d >. >. = <. <. A , B >. , <. c , d >. >. )
125	124	eqeq2d 2471	. . . . . . . . . . 11 |- ( b = B -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. ) )
126	125, 37	3anbi13d 1301	. . . . . . . . . 10 |- ( b = B -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
127	126	rexbidv 2968	. . . . . . . . 9 |- ( b = B -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
128	127	2rexbidv 2975	. . . . . . . 8 |- ( b = B -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
129	128	2rexbidv 2975	. . . . . . 7 |- ( b = B -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
130		opeq1 4219	. . . . . . . . . . . . 13 |- ( c = C -> <. c , d >. = <. C , d >. )
131	130	opeq2d 4226	. . . . . . . . . . . 12 |- ( c = C -> <. <. A , B >. , <. c , d >. >. = <. <. A , B >. , <. C , d >. >. )
132	131	eqeq2d 2471	. . . . . . . . . . 11 |- ( c = C -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. ) )
133	132, 43	3anbi13d 1301	. . . . . . . . . 10 |- ( c = C -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
134	133	rexbidv 2968	. . . . . . . . 9 |- ( c = C -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
135	134	2rexbidv 2975	. . . . . . . 8 |- ( c = C -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
136	135	2rexbidv 2975	. . . . . . 7 |- ( c = C -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
137	122, 129, 136	rspc3ev 3223	. . . . . 6 |- ( ( ( A e. P /\ B e. P /\ C e. P ) /\ E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) -> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) )
138	78, 79, 80, 115, 137	syl31anc 1231	. . . . 5 |- ( ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) /\ mu ) -> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) )
139	138	ex 434	. . . 4 |- ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) -> ( mu -> E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
140	77, 139	impbid 191	. . 3 |- ( ( ( A e. P /\ B e. P ) /\ ( C e. P /\ D e. P /\ E e. P ) /\ ( F e. P /\ G e. P /\ H e. P ) ) -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> mu ) )
141	22, 23, 24, 25, 26, 27, 28, 29, 140	syl233anc 1257	. 2 |- ( ph -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> mu ) )
142	21, 141	bitrd 253	1 |- ( ph -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> mu ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1395   e. wcel 1819   E.wrex 2808   <.cop 4038   class class class wbr 4456   {copab 4514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516

This theorem is referenced by:  brafs  28727