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 2145  ∃wrex 3086

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 3087

This theorem is used by:  trust  24455  utoptop  24460  metustto  24779  restmetu  24796  tgbtwndiff  28848  legov  28927  legso  28941  tglnne  28975  tglndim0  28976  tglinethru  28983  tglinesseq  28987  tglnne0  28988  tglnpt2  29000  footexALT  29072  footex  29075  midex  29092  opptgdim2  29100  plngrnssp  29136  lnssplng  29149  plng3p  29154  cgrane1  29198  cgrane2  29199  cgrane3  29200  cgrane4  29201  cgrahl1  29202  cgrahl2  29203  cgracgr  29204  cgratr  29209  cgrabtwn  29213  cgrahl  29214  dfcgra2  29217  sacgr  29218  acopyeu  29221  cgrarag  29223  ragsupplcgra  29224  cgraer  29256  cgrabasimass  29257  angmgmaddcpbl  29269  angmgmaddcl  29270  angmgmaddlid  29271  angmgmaddrid  29272  angmgm  29276  dfprlng3  29305  f1otrge  29328  suppovss  33153  elq2  33282  cyc3genpm  33592  cyc3conja  33597  archiabllem2c  33635  elrgspnsubrunlem2  33688  rloccring  33711  rloc1r  33713  fracfld  33749  ringlsmss1  33827  ringlsmss2  33828  mxidlprm  33873  qsdrngilem  33896  zringfrac  33964  lindsunlem  34134  dimkerim  34137  cos9thpiminplylem2  34293  txomap  34344  qtophaus  34346  pstmfval  34406  eulerpartlemgvv  34887  tgoldbachgtd  35170  primrootscoprmpow  42965  posbezout  42966  primrootscoprbij2  42969  primrootspoweq0  42972  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c6lem3  43038  aks6d1c6lem5  43043  irrapxlem4  43666