Metamath Proof Explorer

Theorem r3al

Description: Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995) (Proof shortened by Wolf Lammen, 30-Dec-2019)

		Ref	Expression
	Assertion	r3al	$⊢ \forall x \in A \forall y \in B \forall z \in C φ \leftrightarrow \forall x \forall y \forall z ((x \in A \land y \in B \land z \in C) \to φ)$

Proof

Step	Hyp	Ref	Expression
1		r2al	$⊢ \forall x \in A \forall y \in B \forall z \in C φ \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to \forall z \in C φ)$
2		19.21v	$⊢ \forall z ((x \in A \land y \in B) \to (z \in C \to φ)) \leftrightarrow ((x \in A \land y \in B) \to \forall z (z \in C \to φ))$
3		df-3an	$⊢ (x \in A \land y \in B \land z \in C) \leftrightarrow ((x \in A \land y \in B) \land z \in C)$
4	3	imbi1i	$⊢ ((x \in A \land y \in B \land z \in C) \to φ) \leftrightarrow (((x \in A \land y \in B) \land z \in C) \to φ)$
5		impexp	$⊢ (((x \in A \land y \in B) \land z \in C) \to φ) \leftrightarrow ((x \in A \land y \in B) \to (z \in C \to φ))$
6	4 5	bitri	$⊢ ((x \in A \land y \in B \land z \in C) \to φ) \leftrightarrow ((x \in A \land y \in B) \to (z \in C \to φ))$
7	6	albii	$⊢ \forall z ((x \in A \land y \in B \land z \in C) \to φ) \leftrightarrow \forall z ((x \in A \land y \in B) \to (z \in C \to φ))$
8		df-ral	$⊢ \forall z \in C φ \leftrightarrow \forall z (z \in C \to φ)$
9	8	imbi2i	$⊢ ((x \in A \land y \in B) \to \forall z \in C φ) \leftrightarrow ((x \in A \land y \in B) \to \forall z (z \in C \to φ))$
10	2 7 9	3bitr4ri	$⊢ ((x \in A \land y \in B) \to \forall z \in C φ) \leftrightarrow \forall z ((x \in A \land y \in B \land z \in C) \to φ)$
11	10	2albii	$⊢ \forall x \forall y ((x \in A \land y \in B) \to \forall z \in C φ) \leftrightarrow \forall x \forall y \forall z ((x \in A \land y \in B \land z \in C) \to φ)$
12	1 11	bitri	$⊢ \forall x \in A \forall y \in B \forall z \in C φ \leftrightarrow \forall x \forall y \forall z ((x \in A \land y \in B \land z \in C) \to φ)$