Theorem wl-alanbii

Description: This theorem extends alanimi to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019)

	Ref	Expression
Hypothesis	wl-alanbii.1	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
Assertion	wl-alanbii	$$⊢\forall x\phi \leftrightarrow \left(\forall x\psi \wedge \forall x\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-alanbii.1	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
2	1	albii	$$⊢\forall x\phi \leftrightarrow \forall x\left(\psi \wedge \chi \right)$$
3		19.26	$$⊢\forall x\left(\psi \wedge \chi \right)\leftrightarrow \left(\forall x\psi \wedge \forall x\chi \right)$$
4	2 3	bitri	$$⊢\forall x\phi \leftrightarrow \left(\forall x\psi \wedge \forall x\chi \right)$$