Theorem r19.29vva 3197

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  trust  24194  utoptop  24199  metustto  24518  restmetu  24535  tgbtwndiff  28574  legov  28653  legso  28667  tglnne  28696  tglndim0  28697  tglinethru  28704  tglnne0  28708  tglnpt2  28709  footexALT  28786  footex  28789  midex  28805  opptgdim2  28813  cgrane1  28880  cgrane2  28881  cgrane3  28882  cgrane4  28883  cgrahl1  28884  cgrahl2  28885  cgracgr  28886  cgratr  28891  cgrabtwn  28894  cgrahl  28895  dfcgra2  28898  sacgr  28899  acopyeu  28902  f1otrge  28940  suppovss  32754  elq2  32885  cyc3genpm  33213  cyc3conja  33218  archiabllem2c  33256  elrgspnsubrunlem2  33309  rloccring  33331  rloc1r  33333  fracfld  33369  ringlsmss1  33456  ringlsmss2  33457  mxidlprm  33530  qsdrngilem  33554  zringfrac  33614  lindsunlem  33768  dimkerim  33771  cos9thpiminplylem2  33927  txomap  33978  qtophaus  33980  pstmfval  34040  eulerpartlemgvv  34520  tgoldbachgtd  34806  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij2  42542  primrootspoweq0  42545  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c6lem3  42611  aks6d1c6lem5  42616  irrapxlem4  43253