Theorem 3ralbii

Description: Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019)

	Ref	Expression
Hypothesis	3ralbii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	3ralbii	$$⊢\forall x\in A\forall y\in B\forall z\in C\phi \leftrightarrow \forall x\in A\forall y\in B\forall z\in C\psi$$

Proof

Step	Hyp	Ref	Expression
1		3ralbii.1	$$⊢\phi \leftrightarrow \psi$$
2	1	2ralbii	$$⊢\forall y\in B\forall z\in C\phi \leftrightarrow \forall y\in B\forall z\in C\psi$$
3	2	ralbii	$$⊢\forall x\in A\forall y\in B\forall z\in C\phi \leftrightarrow \forall x\in A\forall y\in B\forall z\in C\psi$$