Theorem 19.26-3an
Theorem 19.26 with triple conjunction. (Contributed by NM,
13-Sep-2011.)
Conclusion
\( \vdash \forall x \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \forall x \, \varphi \wedge \forall x \, \psi \wedge \forall x \, \chi \)
Proof
19.26
l1
anbi1i _
\( \vdash \forall x \, (\varphi \wedge \psi) \wedge \forall x \, \chi \leftrightarrow \forall x \, \varphi \wedge \forall x \, \psi \wedge \forall x \, \chi \)
df-3an
l3
albii _
\( \vdash \forall x \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \forall x \, (\varphi \wedge \psi \wedge \chi) \)
19.26
\( \vdash \forall x \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \forall x \, (\varphi \wedge \psi) \wedge \forall x \, \chi \)
l5
bitri l3 _
\( \vdash \forall x \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \forall x \, (\varphi \wedge \psi) \wedge \forall x \, \chi \)
df-3an
\( \vdash \forall x \, \varphi \wedge \forall x \, \psi \wedge \forall x \, \chi \leftrightarrow \forall x \, \varphi \wedge \forall x \, \psi \wedge \forall x \, \chi \)
3bitr4i l1 l5 _