Theorem r19.29vva 3216

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

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

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 3071

This theorem is referenced by:  trust  24238  utoptop  24243  metustto  24566  restmetu  24583  tgbtwndiff  28514  legov  28593  legso  28607  tglnne  28636  tglndim0  28637  tglinethru  28644  tglnne0  28648  tglnpt2  28649  footexALT  28726  footex  28729  midex  28745  opptgdim2  28753  cgrane1  28820  cgrane2  28821  cgrane3  28822  cgrane4  28823  cgrahl1  28824  cgrahl2  28825  cgracgr  28826  cgratr  28831  cgrabtwn  28834  cgrahl  28835  dfcgra2  28838  sacgr  28839  acopyeu  28842  f1otrge  28880  suppovss  32690  cyc3genpm  33172  cyc3conja  33177  archiabllem2c  33202  elrgspnsubrunlem2  33252  rloccring  33274  rloc1r  33276  fracfld  33310  ringlsmss1  33424  ringlsmss2  33425  mxidlprm  33498  qsdrngilem  33522  zringfrac  33582  lindsunlem  33675  dimkerim  33678  txomap  33833  qtophaus  33835  pstmfval  33895  eulerpartlemgvv  34378  tgoldbachgtd  34677  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij2  42104  primrootspoweq0  42107  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c6lem3  42173  aks6d1c6lem5  42178  irrapxlem4  42836