Theorem
mpbir2an
Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
mpbir2an.1
\( \vdash \psi \)
mpbir2an.2
\( \vdash \chi \)
mpbir2an.maj
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \varphi \)
Proof
l0
mpbir2an.2
\( \vdash \chi \)
l1
mpbir2an.1
\( \vdash \psi \)
mpbir2an.maj
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
mpbiran
l1
_
\( \vdash \varphi \leftrightarrow \chi \)
mpbir
l0
_
This is the content in the right pane.