Theorem r19.29vva 3201

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  trust  24166  utoptop  24171  metustto  24490  restmetu  24507  tgbtwndiff  28431  legov  28510  legso  28524  tglnne  28553  tglndim0  28554  tglinethru  28561  tglnne0  28565  tglnpt2  28566  footexALT  28643  footex  28646  midex  28662  opptgdim2  28670  cgrane1  28737  cgrane2  28738  cgrane3  28739  cgrane4  28740  cgrahl1  28741  cgrahl2  28742  cgracgr  28743  cgratr  28748  cgrabtwn  28751  cgrahl  28752  dfcgra2  28755  sacgr  28756  acopyeu  28759  f1otrge  28797  suppovss  32604  elq2  32736  cyc3genpm  33109  cyc3conja  33114  archiabllem2c  33139  elrgspnsubrunlem2  33189  rloccring  33211  rloc1r  33213  fracfld  33248  ringlsmss1  33357  ringlsmss2  33358  mxidlprm  33431  qsdrngilem  33455  zringfrac  33515  lindsunlem  33610  dimkerim  33613  cos9thpiminplylem2  33763  txomap  33811  qtophaus  33813  pstmfval  33873  eulerpartlemgvv  34354  tgoldbachgtd  34640  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij2  42062  primrootspoweq0  42065  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c6lem3  42131  aks6d1c6lem5  42136  irrapxlem4  42795