Theorem r19.29vva 3231

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  trust  24354  utoptop  24359  metustto  24678  restmetu  24695  tgbtwndiff  28740  legov  28819  legso  28833  tglnne  28862  tglndim0  28863  tglinethru  28870  tglinesseq  28874  tglnne0  28875  tglnpt2  28887  footexALT  28956  footex  28959  midex  28976  opptgdim2  28984  plngrnssp  29018  lnssplng  29031  plng3p  29036  cgrane1  29079  cgrane2  29080  cgrane3  29081  cgrane4  29082  cgrahl1  29083  cgrahl2  29084  cgracgr  29085  cgratr  29090  cgrabtwn  29093  cgrahl  29094  dfcgra2  29097  sacgr  29098  acopyeu  29101  f1otrge  29161  suppovss  32966  elq2  33096  cyc3genpm  33412  cyc3conja  33417  archiabllem2c  33455  elrgspnsubrunlem2  33508  rloccring  33531  rloc1r  33533  fracfld  33571  ringlsmss1  33650  ringlsmss2  33651  mxidlprm  33697  qsdrngilem  33720  zringfrac  33788  lindsunlem  33958  dimkerim  33961  cos9thpiminplylem2  34117  txomap  34168  qtophaus  34170  pstmfval  34230  eulerpartlemgvv  34710  tgoldbachgtd  34993  primrootscoprmpow  42755  posbezout  42756  primrootscoprbij2  42759  primrootspoweq0  42762  aks6d1c2lem4  42783  aks6d1c2  42786  aks6d1c6lem3  42828  aks6d1c6lem5  42833  irrapxlem4  43443