Theorem r19.29vva 3195

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 3194	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		idd 24	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒))
5	4	rexlimivv 3177	. 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  24093  utoptop  24098  metustto  24417  restmetu  24434  tgbtwndiff  28409  legov  28488  legso  28502  tglnne  28531  tglndim0  28532  tglinethru  28539  tglnne0  28543  tglnpt2  28544  footexALT  28621  footex  28624  midex  28640  opptgdim2  28648  cgrane1  28715  cgrane2  28716  cgrane3  28717  cgrane4  28718  cgrahl1  28719  cgrahl2  28720  cgracgr  28721  cgratr  28726  cgrabtwn  28729  cgrahl  28730  dfcgra2  28733  sacgr  28734  acopyeu  28737  f1otrge  28775  suppovss  32577  elq2  32709  cyc3genpm  33082  cyc3conja  33087  archiabllem2c  33122  elrgspnsubrunlem2  33172  rloccring  33194  rloc1r  33196  fracfld  33231  ringlsmss1  33340  ringlsmss2  33341  mxidlprm  33414  qsdrngilem  33438  zringfrac  33498  lindsunlem  33593  dimkerim  33596  cos9thpiminplylem2  33746  txomap  33797  qtophaus  33799  pstmfval  33859  eulerpartlemgvv  34340  tgoldbachgtd  34626  primrootscoprmpow  42060  posbezout  42061  primrootscoprbij2  42064  primrootspoweq0  42067  aks6d1c2lem4  42088  aks6d1c2  42091  aks6d1c6lem3  42133  aks6d1c6lem5  42138  irrapxlem4  42786