Theorem r19.29vva 3199

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  trust  24212  utoptop  24217  metustto  24536  restmetu  24553  tgbtwndiff  28592  legov  28671  legso  28685  tglnne  28714  tglndim0  28715  tglinethru  28722  tglnne0  28726  tglnpt2  28727  footexALT  28804  footex  28807  midex  28823  opptgdim2  28831  cgrane1  28898  cgrane2  28899  cgrane3  28900  cgrane4  28901  cgrahl1  28902  cgrahl2  28903  cgracgr  28904  cgratr  28909  cgrabtwn  28912  cgrahl  28913  dfcgra2  28916  sacgr  28917  acopyeu  28920  f1otrge  28958  suppovss  32773  elq2  32904  cyc3genpm  33233  cyc3conja  33238  archiabllem2c  33276  elrgspnsubrunlem2  33329  rloccring  33351  rloc1r  33353  fracfld  33392  ringlsmss1  33479  ringlsmss2  33480  mxidlprm  33553  qsdrngilem  33577  zringfrac  33637  lindsunlem  33808  dimkerim  33811  cos9thpiminplylem2  33967  txomap  34018  qtophaus  34020  pstmfval  34080  eulerpartlemgvv  34560  tgoldbachgtd  34846  primrootscoprmpow  42584  posbezout  42585  primrootscoprbij2  42588  primrootspoweq0  42591  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c6lem3  42657  aks6d1c6lem5  42662  irrapxlem4  43270