r19.29vva - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > r19.29vva		Structured version Visualization version GIF version

Theorem r19.29vva 3211

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 ∃wrex 3067

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

This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3068

This theorem is referenced by: trust 24154 utoptop 24159 metustto 24482 restmetu 24499 tgbtwndiff 28330 legov 28409 legso 28423 tglnne 28452 tglndim0 28453 tglinethru 28460 tglnne0 28464 tglnpt2 28465 footexALT 28542 footex 28545 midex 28561 opptgdim2 28569 cgrane1 28636 cgrane2 28637 cgrane3 28638 cgrane4 28639 cgrahl1 28640 cgrahl2 28641 cgracgr 28642 cgratr 28647 cgrabtwn 28650 cgrahl 28651 dfcgra2 28654 sacgr 28655 acopyeu 28658 f1otrge 28696 suppovss 32486 cyc3genpm 32894 cyc3conja 32899 archiabllem2c 32924 rloccring 33009 rloc1r 33011 fracfld 33019 ringlsmss1 33130 ringlsmss2 33131 mxidlprm 33208 qsdrngilem 33230 zringfrac 33277 lindsunlem 33355 dimkerim 33358 txomap 33468 qtophaus 33470 pstmfval 33530 eulerpartlemgvv 34029 tgoldbachgtd 34327 primrootscoprmpow 41602 posbezout 41603 primrootscoprbij2 41606 primrootspoweq0 41609 aks6d1c2lem4 41630 aks6d1c2 41633 aks6d1c6lem3 41676 aks6d1c6lem5 41681 irrapxlem4 42276

W3C validator

	
		OSZAR »