Theorem 2thd

Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.)

Hypotheses
2thd.1
\( \vdash \varphi \rightarrow \psi \)
2thd.2
\( \vdash \varphi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
2thd.1
\( \vdash \varphi \rightarrow \psi \)
l1
2thd.2
\( \vdash \varphi \rightarrow \chi \)
pm5.1im
\( \vdash \psi \rightarrow \chi \rightarrow (\psi \leftrightarrow \chi) \)
sylc l0 l1 _