Express $(A\to B)\land((C\land B)\to A)$ using biconditional Is there a way to express the formula $(A\to B)\land((C\land B)\to A)$ as a biconditional, i.e. as a statement of the form $\phi\leftrightarrow\psi$ for some expressions $\phi(A,C)$, $\psi(B,C)$? Of course one could always set $\psi=\top$ and $\phi=(A\to B)\land((C\land B)\to A)$ but I want something a little less trivial, hence the restriction that $B$ not be present in $\phi$ and $A$ not in $\psi$ (which I will readily relax if there is some other reasonable nontrivial solution). The obvious first attempts are $(C\land A)\leftrightarrow(C\land B)$, which only gives $(C\land A)\to B$ for the forward implication, and $A\leftrightarrow(C\land B)$, which also gives $A\to C$ in the reverse implication.
 A: $
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\\ #1 \quad & \quad \unicode{x201c}\text{#2}\unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\then}{\Rightarrow}
\newcommand{\followsfrom}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$I can't find anything that matches your requirements exactly, but does perhaps $$\tag 0 (C \then A) \;\equiv\; (A \then B) \land (C \then B)$$ fit your bill?
I found this by putting (A => B) && ((C && B) => A) into Wolfram Alpha, which suggested as one minimal form the DNF $$\tag 1 (A \land B) \lor (\lnot A \land \lnot B) \lor (\lnot A \land \lnot C)$$ which readily transforms into the above expression:
$$\calc
\tag 1 (A \land B) \lor (\lnot A \land \lnot B) \lor (\lnot A \land \lnot C)
\calcop={basic property of $\;\equiv\;$}
(A \equiv B) \lor (\lnot A \land \lnot C)
\calcop={$\;\lor\;$ distributes over $\;\equiv\;$}
A \lor (\lnot A \land \lnot C) \;\equiv\; B \lor (\lnot A \land \lnot C)
\calcop={simplify LHS}
\tag{*} A \lor \lnot C \;\equiv\; B \lor (\lnot A \land \lnot C)
\calcop={distribute $\;\lor\;$ over $\;\land\;$ in RHS; introduce $\;\then\;$, three times}
\tag 0 (C \then A) \;\equiv\; (A \then B) \land (C \then B)
\endcalc$$
This is the most 'symmetrical' form that I've been able to find: but I've only been doing this by trial and error.  The shortest form I could find is $\ref *$, or its DeMorgan variant $\;A \lor \lnot C \;\equiv\; B \lor \lnot (A \lor C)\;$.
