Theorem r19.29vva 3197

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  trust  24117  utoptop  24122  metustto  24441  restmetu  24458  tgbtwndiff  28433  legov  28512  legso  28526  tglnne  28555  tglndim0  28556  tglinethru  28563  tglnne0  28567  tglnpt2  28568  footexALT  28645  footex  28648  midex  28664  opptgdim2  28672  cgrane1  28739  cgrane2  28740  cgrane3  28741  cgrane4  28742  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgratr  28750  cgrabtwn  28753  cgrahl  28754  dfcgra2  28757  sacgr  28758  acopyeu  28761  f1otrge  28799  suppovss  32604  elq2  32736  cyc3genpm  33109  cyc3conja  33114  archiabllem2c  33149  elrgspnsubrunlem2  33199  rloccring  33221  rloc1r  33223  fracfld  33258  ringlsmss1  33367  ringlsmss2  33368  mxidlprm  33441  qsdrngilem  33465  zringfrac  33525  lindsunlem  33620  dimkerim  33623  cos9thpiminplylem2  33773  txomap  33824  qtophaus  33826  pstmfval  33886  eulerpartlemgvv  34367  tgoldbachgtd  34653  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij2  42091  primrootspoweq0  42094  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c6lem3  42160  aks6d1c6lem5  42165  irrapxlem4  42813