Theorem pm5.21ndd

Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.)

Hypotheses
pm5.21ndd.1
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
pm5.21ndd.2
\( \vdash \varphi \rightarrow \theta \rightarrow \psi \)
pm5.21ndd.3
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \theta) \)
Proof
l0
pm5.21ndd.3
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
pm5.21ndd.1
l2
con3d _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \neg \chi \)
pm5.21ndd.2
l4
con3d _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \neg \theta \)
pm5.21im
\( \vdash \neg \chi \rightarrow \neg \theta \rightarrow (\chi \leftrightarrow \theta) \)
syl6c l2 l4 _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow (\chi \leftrightarrow \theta) \)
pm2.61d l0 _