Theorem 19.26

Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Conclusion
\( \vdash \forall x \, (\varphi \wedge \psi) \leftrightarrow \forall x \, \varphi \wedge \forall x \, \psi \)
Proof
simpl
l1
alimi _
simpr
alimi _
l4
jca l1 _
id
alanimi _
impbii l4 _