Theorem pm5.21ni

Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypotheses
pm5.21ni.1
\( \vdash \varphi \rightarrow \psi \)
pm5.21ni.2
\( \vdash \chi \rightarrow \psi \)
Conclusion
\( \vdash \neg \psi \rightarrow (\varphi \leftrightarrow \chi) \)
Proof
pm5.21ni.1
l1
con3i _
pm5.21ni.2
con3i _
2falsed l1 _