Theorem r19.29vva 3223

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

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

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 3088

This theorem is used by:  trust  24541  utoptop  24546  metustto  24865  restmetu  24882  tgbtwndiff  28962  legov  29041  legso  29055  tglnne  29089  tglndim0  29090  tglinethru  29097  tglinesseq  29101  tglnne0  29102  tglnpt2  29114  footexALT  29186  footex  29189  midex  29206  opptgdim2  29214  plngrnssp  29250  lnssplng  29263  plng3p  29268  cgrane1  29312  cgrane2  29313  cgrane3  29314  cgrane4  29315  cgrahl1  29316  cgrahl2  29317  cgracgr  29318  cgratr  29323  cgrabtwn  29327  cgrahl  29328  dfcgra2  29331  sacgr  29332  acopyeu  29335  cgrarag  29337  ragsupplcgra  29338  cgraer  29370  cgrabasimass  29371  angmgmaddcpbl  29383  angmgmaddcl  29384  angmgmaddlid  29385  angmgmaddrid  29386  angmgm  29390  dfprlng3  29419  f1otrge  29442  suppovss  33267  elq2  33396  cyc3genpm  33706  cyc3conja  33711  archiabllem2c  33749  elrgspnsubrunlem2  33802  rloccring  33825  rloc1r  33827  fracfld  33863  ringlsmss1  33942  ringlsmss2  33943  mxidlprm  33988  qsdrngilem  34011  zringfrac  34079  lindsunlem  34249  dimkerim  34252  cos9thpiminplylem2  34408  txomap  34459  qtophaus  34461  pstmfval  34521  eulerpartlemgvv  35001  tgoldbachgtd  35284  primrootscoprmpow  43129  posbezout  43130  primrootscoprbij2  43133  primrootspoweq0  43136  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c6lem3  43202  aks6d1c6lem5  43207  irrapxlem4  43811