Theorem r19.29vva 3266

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-ral 3071  df-rex 3072

This theorem is referenced by:  trust  23392  utoptop  23397  metustto  23720  restmetu  23737  tgbtwndiff  26878  legov  26957  legso  26971  tglnne  27000  tglndim0  27001  tglinethru  27008  tglnne0  27012  tglnpt2  27013  footexALT  27090  footex  27093  midex  27109  opptgdim2  27117  cgrane1  27184  cgrane2  27185  cgrane3  27186  cgrane4  27187  cgrahl1  27188  cgrahl2  27189  cgracgr  27190  cgratr  27195  cgrabtwn  27198  cgrahl  27199  dfcgra2  27202  sacgr  27203  acopyeu  27206  f1otrge  27244  suppovss  31026  cyc3genpm  31428  cyc3conja  31433  archiabllem2c  31458  ringlsmss1  31593  ringlsmss2  31594  mxidlprm  31649  lindsunlem  31714  dimkerim  31717  txomap  31793  qtophaus  31795  pstmfval  31855  eulerpartlemgvv  32352  tgoldbachgtd  32651  irrapxlem4  40656