Theorem r19.29vva 3266

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

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

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  trust  23381  utoptop  23386  metustto  23709  restmetu  23726  tgbtwndiff  26867  legov  26946  legso  26960  tglnne  26989  tglndim0  26990  tglinethru  26997  tglnne0  27001  tglnpt2  27002  footexALT  27079  footex  27082  midex  27098  opptgdim2  27106  cgrane1  27173  cgrane2  27174  cgrane3  27175  cgrane4  27176  cgrahl1  27177  cgrahl2  27178  cgracgr  27179  cgratr  27184  cgrabtwn  27187  cgrahl  27188  dfcgra2  27191  sacgr  27192  acopyeu  27195  f1otrge  27233  suppovss  31017  cyc3genpm  31419  cyc3conja  31424  archiabllem2c  31449  ringlsmss1  31584  ringlsmss2  31585  mxidlprm  31640  lindsunlem  31705  dimkerim  31708  txomap  31784  qtophaus  31786  pstmfval  31846  eulerpartlemgvv  32343  tgoldbachgtd  32642  irrapxlem4  40647