Theorem r19.29vva 3198

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

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

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 3055

This theorem is referenced by:  trust  24124  utoptop  24129  metustto  24448  restmetu  24465  tgbtwndiff  28440  legov  28519  legso  28533  tglnne  28562  tglndim0  28563  tglinethru  28570  tglnne0  28574  tglnpt2  28575  footexALT  28652  footex  28655  midex  28671  opptgdim2  28679  cgrane1  28746  cgrane2  28747  cgrane3  28748  cgrane4  28749  cgrahl1  28750  cgrahl2  28751  cgracgr  28752  cgratr  28757  cgrabtwn  28760  cgrahl  28761  dfcgra2  28764  sacgr  28765  acopyeu  28768  f1otrge  28806  suppovss  32611  elq2  32743  cyc3genpm  33116  cyc3conja  33121  archiabllem2c  33156  elrgspnsubrunlem2  33206  rloccring  33228  rloc1r  33230  fracfld  33265  ringlsmss1  33374  ringlsmss2  33375  mxidlprm  33448  qsdrngilem  33472  zringfrac  33532  lindsunlem  33627  dimkerim  33630  cos9thpiminplylem2  33780  txomap  33831  qtophaus  33833  pstmfval  33893  eulerpartlemgvv  34374  tgoldbachgtd  34660  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij2  42098  primrootspoweq0  42101  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c6lem3  42167  aks6d1c6lem5  42172  irrapxlem4  42820