Theorem r19.29vva 3227

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  trust  24437  utoptop  24442  metustto  24761  restmetu  24778  tgbtwndiff  28826  legov  28905  legso  28919  tglnne  28952  tglndim0  28953  tglinethru  28960  tglinesseq  28964  tglnne0  28965  tglnpt2  28977  footexALT  29049  footex  29052  midex  29069  opptgdim2  29077  plngrnssp  29112  lnssplng  29125  plng3p  29130  cgrane1  29174  cgrane2  29175  cgrane3  29176  cgrane4  29177  cgrahl1  29178  cgrahl2  29179  cgracgr  29180  cgratr  29185  cgrabtwn  29188  cgrahl  29189  dfcgra2  29192  sacgr  29193  acopyeu  29196  cgrarag  29198  ragsupplcgra  29199  dfprlng3  29253  f1otrge  29276  suppovss  33097  elq2  33226  cyc3genpm  33536  cyc3conja  33541  archiabllem2c  33579  elrgspnsubrunlem2  33632  rloccring  33655  rloc1r  33657  fracfld  33693  ringlsmss1  33771  ringlsmss2  33772  mxidlprm  33817  qsdrngilem  33840  zringfrac  33908  lindsunlem  34078  dimkerim  34081  cos9thpiminplylem2  34237  txomap  34288  qtophaus  34290  pstmfval  34350  eulerpartlemgvv  34831  tgoldbachgtd  35114  primrootscoprmpow  42924  posbezout  42925  primrootscoprbij2  42928  primrootspoweq0  42931  aks6d1c2lem4  42952  aks6d1c2  42955  aks6d1c6lem3  42997  aks6d1c6lem5  43002  irrapxlem4  43610