While I understand $\frac{1}{0}$ is undefined, I am unsure how undefined expressions are treated when they occur in antecedents.
For example, is the following statement true?
If $\frac{1}{0} = 3$ then $0 = 0$.
The antecedent $\frac{1}{0} = 3$ is meaningless. Is that a problem?
One thing that suggests to me it is true is the contrapositive appears to be true:
If $0 \neq 0$ then $\frac{1}{0} \neq 3$.
The divisor is in the domain of division because we may assume $0 \neq 0$. The entire statement is true because the antecedent is false.
I found a this previous question which involved variables making the statement meaningless in certain cases. I specifically made sure not to include any variables in my examples so it would get directly to the question of what happens when the antecedent is completely undefined.
Edit 1: Added in response to Mauro ALLEGRANZA. What happens when the conditional only makes sense when taken as a whole because the consequent depends on the antecedent?
As an example, start with multiplicative inverse:
$\forall a\in R, a \neq 0 \rightarrow a a^{-1} = 1$
This seems fine. Let's try some logically equivalent statements:
$\forall a\in R, a a^{-1} \neq 1 \rightarrow a = 0$
This is the contrapositive of the implication. Is this still OK?
$\forall a\in R, a = 0 \lor a a^{-1} = 1$
This uses $A \rightarrow B$ defined as $\neg A \lor B$.
$\forall a\in R, a \neq 0 \lor a a^{-1} = 1 \leftrightarrow a a^{-1} = 1$
This is equivalent in intuitionistic logic as well.
Logically, all these statements should be equivalent. Are they? They all have parts which are undefined when taken in isolation, but the first is clearly defined when taken as a whole. Is there something I'm missing?
It depends on what logical framework you're working in and how you defined $\frac{x}{y}$.
In a type theoretic context, things would typically be arranged so that $\frac{1}{0}$ was a type error which would cause the whole formula to not be a well-formed formula. In that case, it makes about as much sense to ask whether it is true or false as it does to ask whether $x+)=+$ is true or false.
In the more common set-theoretic context, there are a couple of ways of modeling $\frac{x}{y}$. One approach that's not that commonly used and has some issues is to simply define $\frac{x}{0}$ to be some "extra" element that isn't a rational number, say $\bot$. This has the benefit that $\frac{1}{0}$ is a meaningful term, but it leads to things like $\frac{1}{0}=\frac{2}{0}$ and you have to then figure out what $\bot+3$, i.e. $\frac{1}{0}+3$, means.
The most likely approach to be used in a set-theoretic context is related to how functions are viewed set-theoretically. In set theory, a function $f : X \to Y$ is modeled as a set of pairs, i.e. a binary relation, which is total $(\forall x\in X.\exists y.(x,y)\in f)$ and functional $(\forall x,y,y'.(x,y)\in f\land (x,y')\in f\Rightarrow y=y')$. When we say $f(x)=y$, we mean $(x,y)\in f$. If we drop the totality condition, we get a partial function. We can defined $\frac{x}{y}$ via a partial function, $d$ so that $d(x,y)=\frac{x}{y}$, where $\forall x,q.((x,0),q)\notin d$. If we view $d(x,y)=q$ as an abbreviation for $((x,y),q)\in d$ then $d(x,0)=q$ is false.
This last approach makes a lot of sense conceptually, $\frac{x}{y}$ just doesn't map to anything when $y=0$, and it does more or less behave as we would like, but it has some drawbacks. The root of these drawbacks is that this approach means $\frac{x}{y}$ can't be treated as a term unless we guarantee $y\neq 0$. We have already seen that $\frac{x}{y}=q$ gets translated into something not involving equality. As a consequence, we can't use the rules for equality for such expressions. For example, $\frac{1}{0}=\frac{1}{0}$ means $\exists q.((1,0),q)\in d\land ((1,0),q)\in d$ which is false. Similarly, we probably don't want $\frac{1}{0}\neq q$ to mean $\neg(\frac{1}{0}=q)$, i.e. $((1,0),q)\notin d$, but rather $\exists q'.((1,0),q')\in d\land q\neq q'$ which would mean both $\frac{1}{0}=q$ and $\frac{1}{0}\neq q$ would be false. Compound expressions like $\frac{1}{0}+3 = 4$ would mean $\exists q.((1,0),q)\in d\land q+3=4$ which is false. The upshot is roughly that most formulas involving dividing by $0$ become false. There is a straightforward mechanical process to unfold the expressions into relational formulas.
Your contrapositive is $0\neq 0\implies \neg(\frac{1}{0}=3)$, not that it matters because the antecedent is false, but the consequent is actually true when we translate $\frac{1}{0}=3$ as above. It means that $((1,0),3)\notin d$, but this is different from what we want $\frac{1}{0}\neq 3$ to mean. Of course, as I said in the previous paragraph, we can directly see that $\frac{1}{0}=3$ is false, so we can immediately tell that $\frac{1}{0}=3\implies 0=0$ is vacuously true. But if you had used the contrapositive of $\frac{1}{0}=3\implies 0\neq 0$, then the difference between $\neg(\frac{1}{0}=3)$ and $\frac{1}{0}\neq 3$ would become relevant. The former is true, the latter is false.