Theorem r19.29vva 3213

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  trust  23725  utoptop  23730  metustto  24053  restmetu  24070  tgbtwndiff  27746  legov  27825  legso  27839  tglnne  27868  tglndim0  27869  tglinethru  27876  tglnne0  27880  tglnpt2  27881  footexALT  27958  footex  27961  midex  27977  opptgdim2  27985  cgrane1  28052  cgrane2  28053  cgrane3  28054  cgrane4  28055  cgrahl1  28056  cgrahl2  28057  cgracgr  28058  cgratr  28063  cgrabtwn  28066  cgrahl  28067  dfcgra2  28070  sacgr  28071  acopyeu  28074  f1otrge  28112  suppovss  31893  cyc3genpm  32298  cyc3conja  32303  archiabllem2c  32328  ringlsmss1  32494  ringlsmss2  32495  mxidlprm  32574  qsdrngilem  32596  lindsunlem  32697  dimkerim  32700  txomap  32802  qtophaus  32804  pstmfval  32864  eulerpartlemgvv  33363  tgoldbachgtd  33662  irrapxlem4  41548