Theorem ralxp3

Description: Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 2-Feb-2025)

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

Proof

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