Theorem sban

Conjunction inside and outside of a substitution are equivalent. Compare 19.26. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.)

Conclusion
\( \vdash [ y' / x ] \, (\varphi \wedge \psi) \leftrightarrow [ y' / x ] \, \varphi \wedge [ y' / x ] \, \psi \)
Proof
simpl
l1
sbimi _
simpr
sbimi _
l4
jca l1 _
pm3.2
sb2imi _
imp _
impbii l4 _