Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> C e. _V ) |
2 |
1
|
a1i |
|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( A e. _V /\ B e. _V /\ C e. _V ) -> C e. _V ) ) |
3 |
|
simp3 |
|- ( ( R e. _V /\ S e. _V /\ T e. _V ) -> T e. _V ) |
4 |
|
oteqex2 |
|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( C e. _V <-> T e. _V ) ) |
5 |
3 4
|
syl5ibr |
|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( R e. _V /\ S e. _V /\ T e. _V ) -> C e. _V ) ) |
6 |
|
opex |
|- <. A , B >. e. _V |
7 |
|
opthg |
|- ( ( <. A , B >. e. _V /\ C e. _V ) -> ( <. <. A , B >. , C >. = <. <. R , S >. , T >. <-> ( <. A , B >. = <. R , S >. /\ C = T ) ) ) |
8 |
6 7
|
mpan |
|- ( C e. _V -> ( <. <. A , B >. , C >. = <. <. R , S >. , T >. <-> ( <. A , B >. = <. R , S >. /\ C = T ) ) ) |
9 |
8
|
simprbda |
|- ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> <. A , B >. = <. R , S >. ) |
10 |
|
opeqex |
|- ( <. A , B >. = <. R , S >. -> ( ( A e. _V /\ B e. _V ) <-> ( R e. _V /\ S e. _V ) ) ) |
11 |
9 10
|
syl |
|- ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( ( A e. _V /\ B e. _V ) <-> ( R e. _V /\ S e. _V ) ) ) |
12 |
4
|
adantl |
|- ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( C e. _V <-> T e. _V ) ) |
13 |
11 12
|
anbi12d |
|- ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( ( ( A e. _V /\ B e. _V ) /\ C e. _V ) <-> ( ( R e. _V /\ S e. _V ) /\ T e. _V ) ) ) |
14 |
|
df-3an |
|- ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( ( A e. _V /\ B e. _V ) /\ C e. _V ) ) |
15 |
|
df-3an |
|- ( ( R e. _V /\ S e. _V /\ T e. _V ) <-> ( ( R e. _V /\ S e. _V ) /\ T e. _V ) ) |
16 |
13 14 15
|
3bitr4g |
|- ( ( C e. _V /\ <. <. A , B >. , C >. = <. <. R , S >. , T >. ) -> ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( R e. _V /\ S e. _V /\ T e. _V ) ) ) |
17 |
16
|
expcom |
|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( C e. _V -> ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( R e. _V /\ S e. _V /\ T e. _V ) ) ) ) |
18 |
2 5 17
|
pm5.21ndd |
|- ( <. <. A , B >. , C >. = <. <. R , S >. , T >. -> ( ( A e. _V /\ B e. _V /\ C e. _V ) <-> ( R e. _V /\ S e. _V /\ T e. _V ) ) ) |