Theorem r19.29vva 3260

Description: A commonly used pattern based on r19.29 3251, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)

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	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
2	1	ex 402	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))
3	2	ralrimiva 3145	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒))
4	3	ralrimiva 3145	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒))
5		r19.29vva.2	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
6	4, 5	r19.29d2r 3259	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓))
7		pm3.35 838	. . . . 5 ⊢ ((𝜓 ∧ (𝜓 → 𝜒)) → 𝜒)
8	7	ancoms 451	. . . 4 ⊢ (((𝜓 → 𝜒) ∧ 𝜓) → 𝜒)
9	8	rexlimivw 3208	. . 3 ⊢ (∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒)
10	9	rexlimivw 3208	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒)
11	6, 10	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157  ∀wral 3087  ∃wrex 3088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3092  df-rex 3093

This theorem is referenced by:  trust  22358  utoptop  22363  metustto  22683  restmetu  22700  tgbtwndiff  25750  legov  25829  legso  25843  tglnne  25872  tglndim0  25873  tglinethru  25880  tglnne0  25884  tglnpt2  25885  footex  25962  midex  25978  opptgdim2  25986  cgrane1  26053  cgrane2  26054  cgrane3  26055  cgrane4  26056  cgrahl1  26057  cgrahl2  26058  cgracgr  26059  cgratr  26064  cgrabtwn  26066  cgrahl  26067  dfcgra2  26070  sacgr  26071  acopyeu  26074  f1otrge  26101  archiabllem2c  30257  txomap  30409  qtophaus  30411  pstmfval  30447  eulerpartlemgvv  30946  tgoldbachgtd  31252  irrapxlem4  38163