Theorem imnot

If a proposition is false, then implying it is equivalent to being false. One of four theorems that can be used to simplify an implication \( \varphi \rightarrow \psi \), the other ones being [ax-1] (true consequent), pm2.21 (false antecedent), pm5.5 (true antecedent). (Contributed by Mario Carneiro, 26-Apr-2019.) (Proof shortened by Wolf Lammen, 26-May-2019.)

Conclusion
\( \vdash \neg \psi \rightarrow (\varphi \rightarrow \psi \leftrightarrow \neg \varphi) \)
Proof
mtt
bicomd _