Theorem r19.29vva 3192

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  trust  24139  utoptop  24144  metustto  24463  restmetu  24480  tgbtwndiff  28479  legov  28558  legso  28572  tglnne  28601  tglndim0  28602  tglinethru  28609  tglnne0  28613  tglnpt2  28614  footexALT  28691  footex  28694  midex  28710  opptgdim2  28718  cgrane1  28785  cgrane2  28786  cgrane3  28787  cgrane4  28788  cgrahl1  28789  cgrahl2  28790  cgracgr  28791  cgratr  28796  cgrabtwn  28799  cgrahl  28800  dfcgra2  28803  sacgr  28804  acopyeu  28807  f1otrge  28845  suppovss  32654  elq2  32786  cyc3genpm  33113  cyc3conja  33118  archiabllem2c  33156  elrgspnsubrunlem2  33207  rloccring  33229  rloc1r  33231  fracfld  33266  ringlsmss1  33353  ringlsmss2  33354  mxidlprm  33427  qsdrngilem  33451  zringfrac  33511  lindsunlem  33629  dimkerim  33632  cos9thpiminplylem2  33788  txomap  33839  qtophaus  33841  pstmfval  33901  eulerpartlemgvv  34381  tgoldbachgtd  34667  primrootscoprmpow  42132  posbezout  42133  primrootscoprbij2  42136  primrootspoweq0  42139  aks6d1c2lem4  42160  aks6d1c2  42163  aks6d1c6lem3  42205  aks6d1c6lem5  42210  irrapxlem4  42858