Theorem mpbiri

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

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