Theorem
3anbi23d
Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
3anbi12d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
3anbi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\eta \wedge \psi \wedge \theta \leftrightarrow \eta \wedge \chi \wedge \tau) \)
Proof
l0
biidd
l1
3anbi12d.1
3anbi12d.2
3anbi123d
l0
l1
_
This is the content in the right pane.