r2alan

Description: Double restricted universal quantification, special case. (Contributed by Peter Mazsa, 17-Jun-2020)

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

Step	Hyp	Ref	Expression
1		impexp	$⊢ (((x \in A \land y \in B) \land φ) \to ψ) \leftrightarrow ((x \in A \land y \in B) \to (φ \to ψ))$
2	1	2albii	$⊢ \forall x \forall y (((x \in A \land y \in B) \land φ) \to ψ) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to (φ \to ψ))$
3		r2al	$⊢ \forall x \in A \forall y \in B (φ \to ψ) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to (φ \to ψ))$
4	2 3	bitr4i	$⊢ \forall x \forall y (((x \in A \land y \in B) \land φ) \to ψ) \leftrightarrow \forall x \in A \forall y \in B (φ \to ψ)$

Metamath Proof Explorer