Theorem rsp2 3254

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

Assertion

Ref	Expression
rsp2	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

Proof of Theorem rsp2

Step	Hyp	Ref	Expression
1		rsp 3225	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑))
2		rsp 3225	. . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → (𝑦 ∈ 𝐵 → 𝜑))
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)))
4	3	impd 410	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  ralcom2  3351  disjxiun  5104  mpocurryd  8248  cmncom  19728  cnmpt21  23558  cnmpt2t  23560  cnmpt22  23561  cnmptcom  23565  frgrwopreglem5ALT  30251  htthlem  30846  qsidomlem2  33424  cplgredgex  35108  disjlem14  38790  prtlem14  38867  islptre  45617  sprsymrelfolem2  47494