| 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 3114, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
| 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 3215 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
| 4 | idd 24 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒)) | |
| 5 | 4 | rexlimivv 3201 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → 𝜒) |
| 6 | 3, 5 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: trust 24238 utoptop 24243 metustto 24566 restmetu 24583 tgbtwndiff 28514 legov 28593 legso 28607 tglnne 28636 tglndim0 28637 tglinethru 28644 tglnne0 28648 tglnpt2 28649 footexALT 28726 footex 28729 midex 28745 opptgdim2 28753 cgrane1 28820 cgrane2 28821 cgrane3 28822 cgrane4 28823 cgrahl1 28824 cgrahl2 28825 cgracgr 28826 cgratr 28831 cgrabtwn 28834 cgrahl 28835 dfcgra2 28838 sacgr 28839 acopyeu 28842 f1otrge 28880 suppovss 32690 cyc3genpm 33172 cyc3conja 33177 archiabllem2c 33202 elrgspnsubrunlem2 33252 rloccring 33274 rloc1r 33276 fracfld 33310 ringlsmss1 33424 ringlsmss2 33425 mxidlprm 33498 qsdrngilem 33522 zringfrac 33582 lindsunlem 33675 dimkerim 33678 txomap 33833 qtophaus 33835 pstmfval 33895 eulerpartlemgvv 34378 tgoldbachgtd 34677 primrootscoprmpow 42100 posbezout 42101 primrootscoprbij2 42104 primrootspoweq0 42107 aks6d1c2lem4 42128 aks6d1c2 42131 aks6d1c6lem3 42173 aks6d1c6lem5 42178 irrapxlem4 42836 |
| Copyright terms: Public domain | W3C validator |