Theorem sb3an
Threefold conjunction inside and outside of a substitution are equivalent.
(Contributed by NM, 14-Dec-2006.)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow [ y' / x ] \, \varphi \wedge [ y' / x ] \, \psi \wedge [ y' / x ] \, \chi \)
Proof
sban
l1
anbi1i _
\( \vdash [ y' / x ] \, (\varphi \wedge \psi) \wedge [ y' / x ] \, \chi \leftrightarrow [ y' / x ] \, \varphi \wedge [ y' / x ] \, \psi \wedge [ y' / x ] \, \chi \)
df-3an
l3
sbbii _
\( \vdash [ y' / x ] \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow [ y' / x ] \, (\varphi \wedge \psi \wedge \chi) \)
sban
\( \vdash [ y' / x ] \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow [ y' / x ] \, (\varphi \wedge \psi) \wedge [ y' / x ] \, \chi \)
l5
bitri l3 _
\( \vdash [ y' / x ] \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow [ y' / x ] \, (\varphi \wedge \psi) \wedge [ y' / x ] \, \chi \)
df-3an
\( \vdash [ y' / x ] \, \varphi \wedge [ y' / x ] \, \psi \wedge [ y' / x ] \, \chi \leftrightarrow [ y' / x ] \, \varphi \wedge [ y' / x ] \, \psi \wedge [ y' / x ] \, \chi \)
3bitr4i l1 l5 _