Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rspc3ev | Structured version Visualization version GIF version |
Description: 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.) |
Ref | Expression |
---|---|
rspc3v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
rspc3v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) |
rspc3v.3 | ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspc3ev | ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1190 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → 𝐴 ∈ 𝑅) | |
2 | simpl2 1191 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → 𝐵 ∈ 𝑆) | |
3 | rspc3v.3 | . . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) | |
4 | 3 | rspcev 3561 | . . 3 ⊢ ((𝐶 ∈ 𝑇 ∧ 𝜓) → ∃𝑧 ∈ 𝑇 𝜃) |
5 | 4 | 3ad2antl3 1186 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑧 ∈ 𝑇 𝜃) |
6 | rspc3v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
7 | 6 | rexbidv 3226 | . . 3 ⊢ (𝑥 = 𝐴 → (∃𝑧 ∈ 𝑇 𝜑 ↔ ∃𝑧 ∈ 𝑇 𝜒)) |
8 | rspc3v.2 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | |
9 | 8 | rexbidv 3226 | . . 3 ⊢ (𝑦 = 𝐵 → (∃𝑧 ∈ 𝑇 𝜒 ↔ ∃𝑧 ∈ 𝑇 𝜃)) |
10 | 7, 9 | rspc2ev 3572 | . 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∃𝑧 ∈ 𝑇 𝜃) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) |
11 | 1, 2, 5, 10 | syl3anc 1370 | 1 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∃wrex 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-3an 1088 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 |
This theorem is referenced by: f1dom3el3dif 7142 wrdl3s3 14677 pmltpclem1 24612 axlowdim 27329 axeuclidlem 27330 upgr3v3e3cycl 28544 br8d 30950 tgoldbachgt 32643 2goelgoanfmla1 33386 br8 33723 br6 33724 3dim1lem5 37480 lplni2 37551 3rspcedvdw 40181 3cubes 40512 jm2.27 40830 |
Copyright terms: Public domain | W3C validator |