Theorem r19.29vva 3193

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

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

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 3058

This theorem is referenced by:  trust  24164  utoptop  24169  metustto  24488  restmetu  24505  tgbtwndiff  28504  legov  28583  legso  28597  tglnne  28626  tglndim0  28627  tglinethru  28634  tglnne0  28638  tglnpt2  28639  footexALT  28716  footex  28719  midex  28735  opptgdim2  28743  cgrane1  28810  cgrane2  28811  cgrane3  28812  cgrane4  28813  cgrahl1  28814  cgrahl2  28815  cgracgr  28816  cgratr  28821  cgrabtwn  28824  cgrahl  28825  dfcgra2  28828  sacgr  28829  acopyeu  28832  f1otrge  28870  suppovss  32686  elq2  32820  cyc3genpm  33162  cyc3conja  33167  archiabllem2c  33205  elrgspnsubrunlem2  33258  rloccring  33280  rloc1r  33282  fracfld  33318  ringlsmss1  33405  ringlsmss2  33406  mxidlprm  33479  qsdrngilem  33503  zringfrac  33563  lindsunlem  33709  dimkerim  33712  cos9thpiminplylem2  33868  txomap  33919  qtophaus  33921  pstmfval  33981  eulerpartlemgvv  34461  tgoldbachgtd  34747  primrootscoprmpow  42265  posbezout  42266  primrootscoprbij2  42269  primrootspoweq0  42272  aks6d1c2lem4  42293  aks6d1c2  42296  aks6d1c6lem3  42338  aks6d1c6lem5  42343  irrapxlem4  42982