Theorem 2rspcedvdw 3604

Description: Double application of rspcedvdw 3593. (Contributed by SN, 24-Aug-2024.)

Hypotheses

Ref	Expression
2rspcedvdw.1	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
2rspcedvdw.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
2rspcedvdw.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
2rspcedvdw.b	⊢ (𝜑 → 𝐵 ∈ 𝑌)
2rspcedvdw.3	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
2rspcedvdw	⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝜓)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵   𝑥,𝑋   𝑥,𝑌,𝑦   𝜒,𝑥   𝜃,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝜒(𝑦)   𝜃(𝑥)   𝐵(𝑥)   𝑋(𝑦)

Proof of Theorem 2rspcedvdw

Step	Hyp	Ref	Expression
1		2rspcedvdw.a	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
2		2rspcedvdw.b	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑌)
3		2rspcedvdw.3	. 2 ⊢ (𝜑 → 𝜃)
4		2rspcedvdw.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
5		2rspcedvdw.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
6	4, 5	rspc2ev 3603	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝜃) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝜓)
7	1, 2, 3, 6	syl3anc 1396	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096

This theorem is referenced by:  rspc3ev  3607  2sqnn0  27568  z12addscl  28636  z12shalf  28639  z12zsodd  28641  elq2  33097  gsumwun  33337  elrgspnlem2  33504  elrspunsn  33681  posbezout  42791  flt4lem7  43317  nna4b4nsq  43318  nprmmul2  48200  usgrgrtrirex  48638  gpg3kgrtriex  48777  grlimedgnedg  48819