Theorem r19.29vva 3189

Description: A commonly used pattern based on r19.29 3092, 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 3188	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		idd 24	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒))
5	4	rexlimivv 3171	. 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  24115  utoptop  24120  metustto  24439  restmetu  24456  tgbtwndiff  28451  legov  28530  legso  28544  tglnne  28573  tglndim0  28574  tglinethru  28581  tglnne0  28585  tglnpt2  28586  footexALT  28663  footex  28666  midex  28682  opptgdim2  28690  cgrane1  28757  cgrane2  28758  cgrane3  28759  cgrane4  28760  cgrahl1  28761  cgrahl2  28762  cgracgr  28763  cgratr  28768  cgrabtwn  28771  cgrahl  28772  dfcgra2  28775  sacgr  28776  acopyeu  28779  f1otrge  28817  suppovss  32623  elq2  32756  cyc3genpm  33094  cyc3conja  33099  archiabllem2c  33137  elrgspnsubrunlem2  33188  rloccring  33210  rloc1r  33212  fracfld  33247  ringlsmss1  33333  ringlsmss2  33334  mxidlprm  33407  qsdrngilem  33431  zringfrac  33491  lindsunlem  33591  dimkerim  33594  cos9thpiminplylem2  33750  txomap  33801  qtophaus  33803  pstmfval  33863  eulerpartlemgvv  34344  tgoldbachgtd  34630  primrootscoprmpow  42072  posbezout  42073  primrootscoprbij2  42076  primrootspoweq0  42079  aks6d1c2lem4  42100  aks6d1c2  42103  aks6d1c6lem3  42145  aks6d1c6lem5  42150  irrapxlem4  42798