Theorem r19.29vva 3222

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  trust  24259  utoptop  24264  metustto  24587  restmetu  24604  tgbtwndiff  28532  legov  28611  legso  28625  tglnne  28654  tglndim0  28655  tglinethru  28662  tglnne0  28666  tglnpt2  28667  footexALT  28744  footex  28747  midex  28763  opptgdim2  28771  cgrane1  28838  cgrane2  28839  cgrane3  28840  cgrane4  28841  cgrahl1  28842  cgrahl2  28843  cgracgr  28844  cgratr  28849  cgrabtwn  28852  cgrahl  28853  dfcgra2  28856  sacgr  28857  acopyeu  28860  f1otrge  28898  suppovss  32697  cyc3genpm  33145  cyc3conja  33150  archiabllem2c  33175  rloccring  33242  rloc1r  33244  fracfld  33275  ringlsmss1  33389  ringlsmss2  33390  mxidlprm  33463  qsdrngilem  33487  zringfrac  33547  lindsunlem  33637  dimkerim  33640  txomap  33780  qtophaus  33782  pstmfval  33842  eulerpartlemgvv  34341  tgoldbachgtd  34639  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij2  42060  primrootspoweq0  42063  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c6lem3  42129  aks6d1c6lem5  42134  irrapxlem4  42781