![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 4exdistrv | Structured version Visualization version GIF version |
Description: Distribute two pairs of existential quantifiers (over disjoint variables) over a conjunction. For a version with fewer disjoint variable conditions but requiring more axioms, see ee4anv 2348. (Contributed by BJ, 5-Jan-2023.) |
Ref | Expression |
---|---|
4exdistrv | ⊢ (∃𝑥∃𝑧∃𝑦∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistrv 1960 | . . 3 ⊢ (∃𝑦∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ ∃𝑤𝜓)) | |
2 | 1 | 2exbii 1852 | . 2 ⊢ (∃𝑥∃𝑧∃𝑦∃𝑤(𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑧(∃𝑦𝜑 ∧ ∃𝑤𝜓)) |
3 | exdistrv 1960 | . 2 ⊢ (∃𝑥∃𝑧(∃𝑦𝜑 ∧ ∃𝑤𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) | |
4 | 2, 3 | bitri 275 | 1 ⊢ (∃𝑥∃𝑧∃𝑦∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∃wex 1782 |
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 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: cgsex4g 3493 cgsex4gOLD 3494 3oalem3 30648 |
Copyright terms: Public domain | W3C validator |