This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rsp2

Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997)

		Ref	Expression
	Assertion	rsp2	$⊢ \forall x \in A \forall y \in B φ \to ((x \in A \land y \in B) \to φ)$

Step	Hyp	Ref	Expression
1		rsp	$⊢ \forall x \in A \forall y \in B φ \to (x \in A \to \forall y \in B φ)$
2		rsp	$⊢ \forall y \in B φ \to (y \in B \to φ)$
3	1 2	syl6	$⊢ \forall x \in A \forall y \in B φ \to (x \in A \to (y \in B \to φ))$
4	3	impd	$⊢ \forall x \in A \forall y \in B φ \to ((x \in A \land y \in B) \to φ)$