Theorem r19.29vva 3336

Description: A commonly used pattern based on r19.29 3254, 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 3278	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		id 22	. . . 4 ⊢ (𝜒 → 𝜒)
5	4	rexlimivw 3282	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 → 𝜒)
6	5	reximi 3243	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → ∃𝑥 ∈ 𝐴 𝜒)
7	4	rexlimivw 3282	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜒 → 𝜒)
8	3, 6, 7	3syl 18	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  trust  22838  utoptop  22843  metustto  23163  restmetu  23180  tgbtwndiff  26292  legov  26371  legso  26385  tglnne  26414  tglndim0  26415  tglinethru  26422  tglnne0  26426  tglnpt2  26427  footexALT  26504  footex  26507  midex  26523  opptgdim2  26531  cgrane1  26598  cgrane2  26599  cgrane3  26600  cgrane4  26601  cgrahl1  26602  cgrahl2  26603  cgracgr  26604  cgratr  26609  cgrabtwn  26612  cgrahl  26613  dfcgra2  26616  sacgr  26617  acopyeu  26620  f1otrge  26658  suppovss  30426  cyc3genpm  30794  cyc3conja  30799  archiabllem2c  30824  mxidlprm  30977  lindsunlem  31020  dimkerim  31023  txomap  31098  qtophaus  31100  pstmfval  31136  eulerpartlemgvv  31634  tgoldbachgtd  31933  irrapxlem4  39442