Theorem pm5.21nd

Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)

Hypotheses
pm5.21nd.1
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
pm5.21nd.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
pm5.21nd.3
\( \vdash \theta \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
pm5.21nd.1
l1
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
pm5.21nd.2
l3
ex _
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
pm5.21nd.3
a1i _
\( \vdash \varphi \rightarrow \theta \rightarrow (\psi \leftrightarrow \chi) \)
pm5.21ndd l1 l3 _