Theorem r19.29vva 3263

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  trust  23289  utoptop  23294  metustto  23615  restmetu  23632  tgbtwndiff  26771  legov  26850  legso  26864  tglnne  26893  tglndim0  26894  tglinethru  26901  tglnne0  26905  tglnpt2  26906  footexALT  26983  footex  26986  midex  27002  opptgdim2  27010  cgrane1  27077  cgrane2  27078  cgrane3  27079  cgrane4  27080  cgrahl1  27081  cgrahl2  27082  cgracgr  27083  cgratr  27088  cgrabtwn  27091  cgrahl  27092  dfcgra2  27095  sacgr  27096  acopyeu  27099  f1otrge  27137  suppovss  30919  cyc3genpm  31321  cyc3conja  31326  archiabllem2c  31351  ringlsmss1  31486  ringlsmss2  31487  mxidlprm  31542  lindsunlem  31607  dimkerim  31610  txomap  31686  qtophaus  31688  pstmfval  31748  eulerpartlemgvv  32243  tgoldbachgtd  32542  irrapxlem4  40563