Theorem r19.29vva 3229

Description: A commonly used pattern based on r19.29 3220, 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 397	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))
3	2	ralrimiva 3115	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒))
4	3	ralrimiva 3115	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒))
5		r19.29vva.2	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
6	4, 5	r19.29d2r 3228	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓))
7		pm3.35 804	. . . . 5 ⊢ ((𝜓 ∧ (𝜓 → 𝜒)) → 𝜒)
8	7	ancoms 455	. . . 4 ⊢ (((𝜓 → 𝜒) ∧ 𝜓) → 𝜒)
9	8	rexlimivw 3177	. . 3 ⊢ (∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒)
10	9	rexlimivw 3177	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒)
11	6, 10	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2145  ∀wral 3061  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067

This theorem is referenced by:  trust  22253  utoptop  22258  metustto  22578  restmetu  22595  tgbtwndiff  25622  legov  25701  legso  25715  tglnne  25744  tglndim0  25745  tglinethru  25752  tglnne0  25756  tglnpt2  25757  footex  25834  midex  25850  opptgdim2  25858  cgrane1  25925  cgrane2  25926  cgrane3  25927  cgrane4  25928  cgrahl1  25929  cgrahl2  25930  cgracgr  25931  cgratr  25936  cgrabtwn  25938  cgrahl  25939  dfcgra2  25942  sacgr  25943  acopyeu  25946  f1otrge  25973  archiabllem2c  30089  txomap  30241  qtophaus  30243  pstmfval  30279  eulerpartlemgvv  30778  tgoldbachgtd  31080  irrapxlem4  37915