Theorem ralxp3

Description: Restricted for-all over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Hypothesis	ralxp3.1	$$⊢p=⟨⟨x,y⟩,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralxp3	$$⊢\forall p\in \left(\left(A\times B\right)\times C\right)\phi \leftrightarrow \forall x\in A\forall y\in B\forall z\in C\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxp3.1	$$⊢p=⟨⟨x,y⟩,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
2		nfv	$$⊢Ⅎx\phi$$
3		nfv	$$⊢Ⅎy\phi$$
4		nfv	$$⊢Ⅎz\phi$$
5		nfv	$$⊢Ⅎp\psi$$
6	2 3 4 5 1	ralxp3f	$$⊢\forall p\in \left(\left(A\times B\right)\times C\right)\phi \leftrightarrow \forall x\in A\forall y\in B\forall z\in C\psi$$