Theorem r19.29vva 3198

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  trust  24185  utoptop  24190  metustto  24509  restmetu  24526  tgbtwndiff  28590  legov  28669  legso  28683  tglnne  28712  tglndim0  28713  tglinethru  28720  tglnne0  28724  tglnpt2  28725  footexALT  28802  footex  28805  midex  28821  opptgdim2  28829  cgrane1  28896  cgrane2  28897  cgrane3  28898  cgrane4  28899  cgrahl1  28900  cgrahl2  28901  cgracgr  28902  cgratr  28907  cgrabtwn  28910  cgrahl  28911  dfcgra2  28914  sacgr  28915  acopyeu  28918  f1otrge  28956  suppovss  32771  elq2  32903  cyc3genpm  33246  cyc3conja  33251  archiabllem2c  33289  elrgspnsubrunlem2  33342  rloccring  33364  rloc1r  33366  fracfld  33402  ringlsmss1  33489  ringlsmss2  33490  mxidlprm  33563  qsdrngilem  33587  zringfrac  33647  lindsunlem  33802  dimkerim  33805  cos9thpiminplylem2  33961  txomap  34012  qtophaus  34014  pstmfval  34074  eulerpartlemgvv  34554  tgoldbachgtd  34840  primrootscoprmpow  42469  posbezout  42470  primrootscoprbij2  42473  primrootspoweq0  42476  aks6d1c2lem4  42497  aks6d1c2  42500  aks6d1c6lem3  42542  aks6d1c6lem5  42547  irrapxlem4  43182