Step |
Hyp |
Ref |
Expression |
1 |
|
ovmpox2.1 |
|- ( ( x = A /\ y = B ) -> R = S ) |
2 |
|
ovmpox2.2 |
|- ( y = B -> C = L ) |
3 |
|
ovmpox2.3 |
|- F = ( x e. C , y e. D |-> R ) |
4 |
3
|
a1i |
|- ( ( A e. L /\ B e. D /\ S e. H ) -> F = ( x e. C , y e. D |-> R ) ) |
5 |
1
|
adantl |
|- ( ( ( A e. L /\ B e. D /\ S e. H ) /\ ( x = A /\ y = B ) ) -> R = S ) |
6 |
2
|
adantl |
|- ( ( ( A e. L /\ B e. D /\ S e. H ) /\ y = B ) -> C = L ) |
7 |
|
simp1 |
|- ( ( A e. L /\ B e. D /\ S e. H ) -> A e. L ) |
8 |
|
simp2 |
|- ( ( A e. L /\ B e. D /\ S e. H ) -> B e. D ) |
9 |
|
simp3 |
|- ( ( A e. L /\ B e. D /\ S e. H ) -> S e. H ) |
10 |
4 5 6 7 8 9
|
ovmpordx |
|- ( ( A e. L /\ B e. D /\ S e. H ) -> ( A F B ) = S ) |