Theorem r19.29vva 3196

Description: A commonly used pattern based on r19.29 3099, 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 3195	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		idd 24	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒))
5	4	rexlimivv 3178	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → 𝜒)
6	3, 5	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  trust  24173  utoptop  24178  metustto  24497  restmetu  24514  tgbtwndiff  28578  legov  28657  legso  28671  tglnne  28700  tglndim0  28701  tglinethru  28708  tglnne0  28712  tglnpt2  28713  footexALT  28790  footex  28793  midex  28809  opptgdim2  28817  cgrane1  28884  cgrane2  28885  cgrane3  28886  cgrane4  28887  cgrahl1  28888  cgrahl2  28889  cgracgr  28890  cgratr  28895  cgrabtwn  28898  cgrahl  28899  dfcgra2  28902  sacgr  28903  acopyeu  28906  f1otrge  28944  suppovss  32760  elq2  32892  cyc3genpm  33234  cyc3conja  33239  archiabllem2c  33277  elrgspnsubrunlem2  33330  rloccring  33352  rloc1r  33354  fracfld  33390  ringlsmss1  33477  ringlsmss2  33478  mxidlprm  33551  qsdrngilem  33575  zringfrac  33635  lindsunlem  33781  dimkerim  33784  cos9thpiminplylem2  33940  txomap  33991  qtophaus  33993  pstmfval  34053  eulerpartlemgvv  34533  tgoldbachgtd  34819  primrootscoprmpow  42353  posbezout  42354  primrootscoprbij2  42357  primrootspoweq0  42360  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c6lem3  42426  aks6d1c6lem5  42431  irrapxlem4  43067