Universal Quantifier Distributes over Conjunction

Theorem

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.

Then:

$\forall x: \paren {\map \phi x \land \map \psi x} \dashv \vdash \paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$

Proof

Forward Implication

By the tableau method of natural deduction:

$\forall x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x} $

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\forall x: \paren {\map \phi x \land \map \psi x}$	Premise
2		1	$\map \phi {x \gets x_0} \land \map \psi {x \gets x_0}$	Universal Instantiation	1
3		1	$\map \phi {x \gets x_0}$	Rule of Simplification	2
4		1	$\forall x: \map \phi x$	Universal Generalisation	3
5		1	$\map \psi {x \gets x_0}$	Rule of Simplification	2
6		1	$\forall x: \map \psi x$	Universal Generalisation	5
7		1	$\paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$	Rule of Conjunction	4, 6

$\Box$

Reverse Implication

By the tableau method of natural deduction:

$\paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x} \vdash \forall x: \paren {\map \phi x \land \map \psi x} $

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$	Premise
2		1	$\forall x: \map \phi x$	Rule of Simplification	1
3		1	$\map \phi {x \gets x_0}$	Universal Instantiation	2
4		1	$\forall x: \map \psi x$	Rule of Simplification	1
5		1	$\map \psi {x \gets x_0}$	Universal Instantiation	4
6		1	$\map \phi {x \gets x_0} \land \map \psi {x \gets x_0}$	Rule of Conjunction	3, 5
7		1	$\forall x: \paren {\map \phi x \land \map \psi x}$	Universal Generalisation	6

$\blacksquare$