Theorem r19.29vva 3225

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  trust  24386  utoptop  24391  metustto  24710  restmetu  24727  tgbtwndiff  28775  legov  28854  legso  28868  tglnne  28901  tglndim0  28902  tglinethru  28909  tglinesseq  28913  tglnne0  28914  tglnpt2  28926  footexALT  28998  footex  29001  midex  29018  opptgdim2  29026  plngrnssp  29061  lnssplng  29074  plng3p  29079  cgrane1  29123  cgrane2  29124  cgrane3  29125  cgrane4  29126  cgrahl1  29127  cgrahl2  29128  cgracgr  29129  cgratr  29134  cgrabtwn  29137  cgrahl  29138  dfcgra2  29141  sacgr  29142  acopyeu  29145  cgrarag  29147  ragsupplcgra  29148  dfprlng3  29198  f1otrge  29221  suppovss  33026  elq2  33156  cyc3genpm  33472  cyc3conja  33477  archiabllem2c  33515  elrgspnsubrunlem2  33568  rloccring  33591  rloc1r  33593  fracfld  33629  ringlsmss1  33707  ringlsmss2  33708  mxidlprm  33753  qsdrngilem  33776  zringfrac  33844  lindsunlem  34014  dimkerim  34017  cos9thpiminplylem2  34173  txomap  34224  qtophaus  34226  pstmfval  34286  eulerpartlemgvv  34766  tgoldbachgtd  35049  primrootscoprmpow  42866  posbezout  42867  primrootscoprbij2  42870  primrootspoweq0  42873  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c6lem3  42939  aks6d1c6lem5  42944  irrapxlem4  43552