Step |
Hyp |
Ref |
Expression |
1 |
|
s2eq2s1eq |
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( <" A "> = <" C "> /\ <" B "> = <" D "> ) ) ) |
2 |
|
s111 |
|- ( ( A e. V /\ C e. V ) -> ( <" A "> = <" C "> <-> A = C ) ) |
3 |
2
|
ad2ant2r |
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A "> = <" C "> <-> A = C ) ) |
4 |
|
s111 |
|- ( ( B e. V /\ D e. V ) -> ( <" B "> = <" D "> <-> B = D ) ) |
5 |
4
|
ad2ant2l |
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" B "> = <" D "> <-> B = D ) ) |
6 |
3 5
|
anbi12d |
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( <" A "> = <" C "> /\ <" B "> = <" D "> ) <-> ( A = C /\ B = D ) ) ) |
7 |
1 6
|
bitrd |
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( A = C /\ B = D ) ) ) |