Theorem r19.29vva 3292

Description: A commonly used pattern based on r19.29 3216, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)

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 3237	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		id 22	. . . 4 ⊢ (𝜒 → 𝜒)
5	4	rexlimivw 3241	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 → 𝜒)
6	5	reximi 3206	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → ∃𝑥 ∈ 𝐴 𝜒)
7	4	rexlimivw 3241	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜒 → 𝜒)
8	3, 6, 7	3syl 18	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  trust  22835  utoptop  22840  metustto  23160  restmetu  23177  tgbtwndiff  26300  legov  26379  legso  26393  tglnne  26422  tglndim0  26423  tglinethru  26430  tglnne0  26434  tglnpt2  26435  footexALT  26512  footex  26515  midex  26531  opptgdim2  26539  cgrane1  26606  cgrane2  26607  cgrane3  26608  cgrane4  26609  cgrahl1  26610  cgrahl2  26611  cgracgr  26612  cgratr  26617  cgrabtwn  26620  cgrahl  26621  dfcgra2  26624  sacgr  26625  acopyeu  26628  f1otrge  26666  suppovss  30443  cyc3genpm  30844  cyc3conja  30849  archiabllem2c  30874  ringlsmss1  31003  ringlsmss2  31004  mxidlprm  31048  lindsunlem  31108  dimkerim  31111  txomap  31187  qtophaus  31189  pstmfval  31249  eulerpartlemgvv  31744  tgoldbachgtd  32043  irrapxlem4  39766