Theorem r19.29vva 3222

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  trust  24286  utoptop  24291  metustto  24610  restmetu  24627  tgbtwndiff  28672  legov  28751  legso  28765  tglnne  28794  tglndim0  28795  tglinethru  28802  tglinesseq  28806  tglnne0  28807  tglnpt2  28819  footexALT  28888  footex  28891  midex  28907  opptgdim2  28915  plngrnssp  28983  lnssplng  28996  plng3p  28997  cgrane1  29003  cgrane2  29004  cgrane3  29005  cgrane4  29006  cgrahl1  29007  cgrahl2  29008  cgracgr  29009  cgratr  29014  cgrabtwn  29017  cgrahl  29018  dfcgra2  29021  sacgr  29022  acopyeu  29025  f1otrge  29069  suppovss  32880  elq2  33011  cyc3genpm  33329  cyc3conja  33334  archiabllem2c  33372  elrgspnsubrunlem2  33426  rloccring  33449  rloc1r  33451  fracfld  33492  ringlsmss1  33579  ringlsmss2  33580  mxidlprm  33655  qsdrngilem  33679  zringfrac  33747  lindsunlem  33918  dimkerim  33921  cos9thpiminplylem2  34077  txomap  34128  qtophaus  34130  pstmfval  34190  eulerpartlemgvv  34670  tgoldbachgtd  34953  primrootscoprmpow  42713  posbezout  42714  primrootscoprbij2  42717  primrootspoweq0  42720  aks6d1c2lem4  42741  aks6d1c2  42744  aks6d1c6lem3  42786  aks6d1c6lem5  42791  irrapxlem4  43399