Metamath Proof Explorer

Theorem rspec3

Description: Specialization rule for restricted quantification, with three quantifiers. (Contributed by NM, 20-Nov-1994)

		Ref	Expression
	Hypothesis	rspec3.1	$⊢ \forall x \in A \forall y \in B \forall z \in C φ$
	Assertion	rspec3	$⊢ (x \in A \land y \in B \land z \in C) \to φ$

Step	Hyp	Ref	Expression
1		rspec3.1	$⊢ \forall x \in A \forall y \in B \forall z \in C φ$
2	1	rspec2	$⊢ (x \in A \land y \in B) \to \forall z \in C φ$
3	2	r19.21bi	$⊢ ((x \in A \land y \in B) \land z \in C) \to φ$
4	3	3impa	$⊢ (x \in A \land y \in B \land z \in C) \to φ$