Theorem r19.29vva 3214

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  trust  23734  utoptop  23739  metustto  24062  restmetu  24079  tgbtwndiff  27757  legov  27836  legso  27850  tglnne  27879  tglndim0  27880  tglinethru  27887  tglnne0  27891  tglnpt2  27892  footexALT  27969  footex  27972  midex  27988  opptgdim2  27996  cgrane1  28063  cgrane2  28064  cgrane3  28065  cgrane4  28066  cgrahl1  28067  cgrahl2  28068  cgracgr  28069  cgratr  28074  cgrabtwn  28077  cgrahl  28078  dfcgra2  28081  sacgr  28082  acopyeu  28085  f1otrge  28123  suppovss  31906  cyc3genpm  32311  cyc3conja  32316  archiabllem2c  32341  ringlsmss1  32506  ringlsmss2  32507  mxidlprm  32586  qsdrngilem  32608  lindsunlem  32709  dimkerim  32712  txomap  32814  qtophaus  32816  pstmfval  32876  eulerpartlemgvv  33375  tgoldbachgtd  33674  irrapxlem4  41563