Theorem r19.29vva 3226

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

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

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 1945

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

This theorem is used by:  trust  24603  utoptop  24608  metustto  24927  restmetu  24944  tgbtwndiff  29026  legov  29105  legso  29119  tglnne  29153  tglndim0  29154  tglinethru  29161  tglinesseq  29165  tglnne0  29166  tglnpt2  29178  footexALT  29250  footex  29253  midex  29270  opptgdim2  29278  plngrnssp  29314  lnssplng  29327  plng3p  29332  cgrane1  29376  cgrane2  29377  cgrane3  29378  cgrane4  29379  cgrahl1  29380  cgrahl2  29381  cgracgr  29382  cgratr  29387  cgrabtwn  29391  cgrahl  29392  dfcgra2  29395  sacgr  29396  acopyeu  29399  cgrarag  29401  ragsupplcgra  29402  cgraer  29434  cgrabasimass  29435  angmgmaddcpbl  29447  angmgmaddcl  29448  angmgmaddlid  29449  angmgmaddrid  29450  angmgm  29454  dfprlng3  29483  f1otrge  29506  cgrahlb  33104  suppovss  33371  elq2  33499  cyc3genpm  33812  cyc3conja  33817  archiabllem2c  33855  elrgspnsubrunlem2  33908  rloccring  33931  rloc1r  33933  edompidlem  33960  fracfld  33974  ringlsmss1  34053  ringlsmss2  34054  mxidlprm  34099  qsdrngilem  34122  zringfrac  34189  lindsunlem  34367  dimkerim  34370  cos9thpiminplylem2  34526  txomap  34577  qtophaus  34579  pstmfval  34639  eulerpartlemgvv  35119  tgoldbachgtd  35402  primrootscoprmpow  43415  posbezout  43416  primrootscoprbij2  43419  primrootspoweq0  43422  aks6d1c2lem4  43443  aks6d1c2  43446  aks6d1c6lem3  43488  aks6d1c6lem5  43493  irrapxlem4  44098