Material biconditional and substitution

Question

Does the material biconditional have the substitution property?

As an example, if I was able to derive $A \leftrightarrow B$ during an argument, may I substitute $A$ for $B$ (or vice-versa) in any previous formula?

Answer 1

Yes. If $\phi(A)$ is some statement with zero or more instances of $A$ as part of it, and $\phi(B)$ the result of substituting any number of those (you don't have to substitute all of them), then if $A \leftrightarrow B$ is true, and $\phi(A)$ is true, then $\phi(B)$ will be true as well.

So yes, if in some proof you have both $A \leftrightarrow B$ and $\phi(A)$, then you can infer $\phi(B)$. Of course, to be able to do this in a purely formal proof requires an explicit inference rule to this effect.