Theorem mpbii

An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses
mpbii.min
\( \vdash \psi \)
mpbii.maj
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
mpbii.min
l1
a1i _
\( \vdash \varphi \rightarrow \psi \)
mpbii.maj
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
mpbid l1 _