Theorem 19.26

Description: 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)

	Ref	Expression
Assertion	19.26	$$⊢\forall x\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\phi \wedge \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(\phi \wedge \psi \right)\to \phi$$
2	1	alimi	$$⊢\forall x\left(\phi \wedge \psi \right)\to \forall x\phi$$
3		simpr	$$⊢\left(\phi \wedge \psi \right)\to \psi$$
4	3	alimi	$$⊢\forall x\left(\phi \wedge \psi \right)\to \forall x\psi$$
5	2 4	jca	$$⊢\forall x\left(\phi \wedge \psi \right)\to \left(\forall x\phi \wedge \forall x\psi \right)$$
6		id	$$⊢\left(\phi \wedge \psi \right)\to \left(\phi \wedge \psi \right)$$
7	6	alanimi	$$⊢\left(\forall x\phi \wedge \forall x\psi \right)\to \forall x\left(\phi \wedge \psi \right)$$
8	5 7	impbii	$$⊢\forall x\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\phi \wedge \forall x\psi \right)$$