Theorem r19.29vva 3212

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  trust  24055  utoptop  24060  metustto  24383  restmetu  24400  tgbtwndiff  28192  legov  28271  legso  28285  tglnne  28314  tglndim0  28315  tglinethru  28322  tglnne0  28326  tglnpt2  28327  footexALT  28404  footex  28407  midex  28423  opptgdim2  28431  cgrane1  28498  cgrane2  28499  cgrane3  28500  cgrane4  28501  cgrahl1  28502  cgrahl2  28503  cgracgr  28504  cgratr  28509  cgrabtwn  28512  cgrahl  28513  dfcgra2  28516  sacgr  28517  acopyeu  28520  f1otrge  28558  suppovss  32341  cyc3genpm  32749  cyc3conja  32754  archiabllem2c  32779  ringlsmss1  32948  ringlsmss2  32949  mxidlprm  33028  qsdrngilem  33050  lindsunlem  33165  dimkerim  33168  txomap  33280  qtophaus  33282  pstmfval  33342  eulerpartlemgvv  33841  tgoldbachgtd  34140  irrapxlem4  42029