Suppose that we have a category $\mathcal{C}$ which "has binary products" (full definition provided here: https://en.wikipedia.org/wiki/Product_(category_theory)). We want to show that given $A, B, C \in \mathcal{C}$ and morphisms $f, g : A \to B \times C$, $$f = g \iff p_1 \circ f = p_1 \circ g \text{ and } p_2 \circ f = p_2 \circ g$$
For the forward direction, I think I have a working proof:
Suppose that $f = g$. Then $\forall x$ $f(x) = g(x)$. Consider arbitrary $x \in A$ and suppose that $f(x) = g(x) = y$. Then $p_1(f(x)) = p_1(y) = p_1(y) = p_1(g(x))$ and similarly, $p_2(f(x)) = p_2(y) = p_2(y) = p_2(g(x))$. Since our choice of $x$ was arbitrary, $p_1 \circ f = p_1 \circ g$ and $p_2 \circ f = p_2 \circ g$.
One concern with the forward direction that I have is that can we really say $p_1 (f(x)) = p_1(y) = p_1(g(x)) \implies p_1(f(x)) = p_1(g(x))$ without knowing injectivity/surjectivity of $f$ and $g$? I think the answer to this question is yes.
For the reverse direction I'm completely stuck. I can't get past the fact that $f : A \to B$ and $p_1 : B \times C \to B$. The inputs and outputs to $p_1$ and $f$ don't match so we can't really have something like $p_1 \circ f$, right? Similar things happen with $g$ as well as $p_2$.
Edit: I was thinking of $f : A \to B$ and $g : A \to C$ but it should be $f, g : A \to B \times C$ as edited above. Still confused about the reverse direction.
Old post but I'll give it a go since no one has put a dedicated answer.
There are two types of axioms. Axioms of the language you are using (logical axioms), and axioms of the theory of interest.
$$ h = k \implies p_a \circ h = p_a \circ k \ \land \ p_b \circ h = p_b \circ k$$
is the result of the logical axioms of first-order logic (See Propositional and Predicate Calculus, Goldrei, Section 5.2, Axioms for equality)
To prove the other direction requires the axioms/theorems of category theory: (I apologize for posting a pdf. I already had an answer typed using tikzcd, which apparently isn't compatible with this site, so I can't upload the $\LaTeX$ code)