Theorem r19.29vva 3223

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-rex 3088

This theorem is referenced by:  trust  24365  utoptop  24370  metustto  24689  restmetu  24706  tgbtwndiff  28751  legov  28830  legso  28844  tglnne  28877  tglndim0  28878  tglinethru  28885  tglinesseq  28889  tglnne0  28890  tglnpt2  28902  footexALT  28973  footex  28976  midex  28993  opptgdim2  29001  plngrnssp  29035  lnssplng  29048  plng3p  29053  cgrane1  29096  cgrane2  29097  cgrane3  29098  cgrane4  29099  cgrahl1  29100  cgrahl2  29101  cgracgr  29102  cgratr  29107  cgrabtwn  29110  cgrahl  29111  dfcgra2  29114  sacgr  29115  acopyeu  29118  cgrarag  29120  ragsupplcgra  29121  dfprlng3  29171  f1otrge  29187  suppovss  32992  elq2  33122  cyc3genpm  33438  cyc3conja  33443  archiabllem2c  33481  elrgspnsubrunlem2  33534  rloccring  33557  rloc1r  33559  fracfld  33595  ringlsmss1  33673  ringlsmss2  33674  mxidlprm  33719  qsdrngilem  33742  zringfrac  33810  lindsunlem  33980  dimkerim  33983  cos9thpiminplylem2  34139  txomap  34190  qtophaus  34192  pstmfval  34252  eulerpartlemgvv  34732  tgoldbachgtd  35015  primrootscoprmpow  42812  posbezout  42813  primrootscoprbij2  42816  primrootspoweq0  42819  aks6d1c2lem4  42840  aks6d1c2  42843  aks6d1c6lem3  42885  aks6d1c6lem5  42890  irrapxlem4  43500