Description: Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv . (Contributed by NM, 31-Jul-1995)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ee4anv | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | excom | ⊢ ( ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ) | |
| 2 | 1 | exbii | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ) |
| 3 | eeanv | ⊢ ( ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑦 𝜑 ∧ ∃ 𝑤 𝜓 ) ) | |
| 4 | 3 | 2exbii | ⊢ ( ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑧 ( ∃ 𝑦 𝜑 ∧ ∃ 𝑤 𝜓 ) ) |
| 5 | eeanv | ⊢ ( ∃ 𝑥 ∃ 𝑧 ( ∃ 𝑦 𝜑 ∧ ∃ 𝑤 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 𝜓 ) ) | |
| 6 | 2 4 5 | 3bitri | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 𝜓 ) ) |