Theorem pm5.21nii

Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)

Hypotheses
pm5.21ni.1
\( \vdash \varphi \rightarrow \psi \)
pm5.21ni.2
\( \vdash \chi \rightarrow \psi \)
pm5.21nii.3
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \)
Proof
l0
pm5.21nii.3
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \)
l1
pm5.21ni.1
pm5.21ni.2
pm5.21ni l1 _
\( \vdash \neg \psi \rightarrow (\varphi \leftrightarrow \chi) \)
pm2.61i l0 _