Theorem r19.29vva 3198

Description: A commonly used pattern based on r19.29 3101, 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 2114  ∃wrex 3062

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 3063

This theorem is referenced by:  trust  24207  utoptop  24212  metustto  24531  restmetu  24548  tgbtwndiff  28591  legov  28670  legso  28684  tglnne  28713  tglndim0  28714  tglinethru  28721  tglnne0  28725  tglnpt2  28726  footexALT  28803  footex  28806  midex  28822  opptgdim2  28830  cgrane1  28897  cgrane2  28898  cgrane3  28899  cgrane4  28900  cgrahl1  28901  cgrahl2  28902  cgracgr  28903  cgratr  28908  cgrabtwn  28911  cgrahl  28912  dfcgra2  28915  sacgr  28916  acopyeu  28919  f1otrge  28957  suppovss  32772  elq2  32903  cyc3genpm  33231  cyc3conja  33236  archiabllem2c  33274  elrgspnsubrunlem2  33327  rloccring  33349  rloc1r  33351  fracfld  33387  ringlsmss1  33474  ringlsmss2  33475  mxidlprm  33548  qsdrngilem  33572  zringfrac  33632  lindsunlem  33787  dimkerim  33790  cos9thpiminplylem2  33946  txomap  33997  qtophaus  33999  pstmfval  34059  eulerpartlemgvv  34539  tgoldbachgtd  34825  primrootscoprmpow  42555  posbezout  42556  primrootscoprbij2  42559  primrootspoweq0  42562  aks6d1c2lem4  42583  aks6d1c2  42586  aks6d1c6lem3  42628  aks6d1c6lem5  42633  irrapxlem4  43274