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 25	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒))
5	4	rexlimivv 3204	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → 𝜒)
6	3, 5	syl 18	1 ⊢ (𝜑 → 𝜒)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  trust  24557  utoptop  24562  metustto  24881  restmetu  24898  tgbtwndiff  28978  legov  29057  legso  29071  tglnne  29105  tglndim0  29106  tglinethru  29113  tglinesseq  29117  tglnne0  29118  tglnpt2  29130  footexALT  29202  footex  29205  midex  29222  opptgdim2  29230  plngrnssp  29266  lnssplng  29279  plng3p  29284  cgrane1  29328  cgrane2  29329  cgrane3  29330  cgrane4  29331  cgrahl1  29332  cgrahl2  29333  cgracgr  29334  cgratr  29339  cgrabtwn  29343  cgrahl  29344  dfcgra2  29347  sacgr  29348  acopyeu  29351  cgrarag  29353  ragsupplcgra  29354  cgraer  29386  cgrabasimass  29387  angmgmaddcpbl  29399  angmgmaddcl  29400  angmgmaddlid  29401  angmgmaddrid  29402  angmgm  29406  dfprlng3  29435  f1otrge  29458  cgrahlb  33056  suppovss  33325  elq2  33453  cyc3genpm  33763  cyc3conja  33768  archiabllem2c  33806  elrgspnsubrunlem2  33859  rloccring  33882  rloc1r  33884  fracfld  33920  ringlsmss1  33999  ringlsmss2  34000  mxidlprm  34045  qsdrngilem  34068  zringfrac  34136  lindsunlem  34306  dimkerim  34309  cos9thpiminplylem2  34465  txomap  34516  qtophaus  34518  pstmfval  34578  eulerpartlemgvv  35058  tgoldbachgtd  35341  primrootscoprmpow  43258  posbezout  43259  primrootscoprbij2  43262  primrootspoweq0  43265  aks6d1c2lem4  43286  aks6d1c2  43289  aks6d1c6lem3  43331  aks6d1c6lem5  43336  irrapxlem4  43941