Theorem r19.29vva 3213

Description: A commonly used pattern based on r19.29 3111, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)

Hypotheses

Ref	Expression
r19.29vva.1	⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
r19.29vva.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Assertion

Ref	Expression
r19.29vva	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝜒   𝜑,𝑥,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem r19.29vva

Step	Hyp	Ref	Expression
1		r19.29vva.1	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
2		r19.29vva.2	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
3	1, 2	reximddv2 3212	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		idd 24	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒))
5	4	rexlimivv 3198	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → 𝜒)
6	3, 5	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  trust  24253  utoptop  24258  metustto  24581  restmetu  24598  tgbtwndiff  28528  legov  28607  legso  28621  tglnne  28650  tglndim0  28651  tglinethru  28658  tglnne0  28662  tglnpt2  28663  footexALT  28740  footex  28743  midex  28759  opptgdim2  28767  cgrane1  28834  cgrane2  28835  cgrane3  28836  cgrane4  28837  cgrahl1  28838  cgrahl2  28839  cgracgr  28840  cgratr  28845  cgrabtwn  28848  cgrahl  28849  dfcgra2  28852  sacgr  28853  acopyeu  28856  f1otrge  28894  suppovss  32695  cyc3genpm  33154  cyc3conja  33159  archiabllem2c  33184  rloccring  33256  rloc1r  33258  fracfld  33289  ringlsmss1  33403  ringlsmss2  33404  mxidlprm  33477  qsdrngilem  33501  zringfrac  33561  lindsunlem  33651  dimkerim  33654  txomap  33794  qtophaus  33796  pstmfval  33856  eulerpartlemgvv  34357  tgoldbachgtd  34655  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij2  42084  primrootspoweq0  42087  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c6lem3  42153  aks6d1c6lem5  42158  irrapxlem4  42812