Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.29vva | Structured version Visualization version GIF version |
Description: A commonly used pattern based on r19.29 3251, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
Ref | Expression |
---|---|
r19.29vva.1 | ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) |
r19.29vva.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Ref | Expression |
---|---|
r19.29vva | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29vva.1 | . . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) | |
2 | r19.29vva.2 | . . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
3 | 1, 2 | reximddv2 3275 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | id 22 | . . . 4 ⊢ (𝜒 → 𝜒) | |
5 | 4 | rexlimivw 3279 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 → 𝜒) |
6 | 5 | reximi 3240 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → ∃𝑥 ∈ 𝐴 𝜒) |
7 | 4 | rexlimivw 3279 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜒 → 𝜒) |
8 | 3, 6, 7 | 3syl 18 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-ral 3140 df-rex 3141 |
This theorem is referenced by: trust 22765 utoptop 22770 metustto 23090 restmetu 23107 tgbtwndiff 26219 legov 26298 legso 26312 tglnne 26341 tglndim0 26342 tglinethru 26349 tglnne0 26353 tglnpt2 26354 footexALT 26431 footex 26434 midex 26450 opptgdim2 26458 cgrane1 26525 cgrane2 26526 cgrane3 26527 cgrane4 26528 cgrahl1 26529 cgrahl2 26530 cgracgr 26531 cgratr 26536 cgrabtwn 26539 cgrahl 26540 dfcgra2 26543 sacgr 26544 acopyeu 26547 f1otrge 26585 suppovss 30354 cyc3genpm 30721 cyc3conja 30726 archiabllem2c 30751 lindsunlem 30919 dimkerim 30922 txomap 30997 qtophaus 30999 pstmfval 31035 eulerpartlemgvv 31533 tgoldbachgtd 31832 irrapxlem4 39300 |
Copyright terms: Public domain | W3C validator |