Theorem 4exdistrv

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 . (Contributed by BJ, 5-Jan-2023)

	Ref	Expression
Assertion	4exdistrv	⊢ ( ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		exdistrv	⊢ ( ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑦 𝜑 ∧ ∃ 𝑤 𝜓 ) )
2	1	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑧 ( ∃ 𝑦 𝜑 ∧ ∃ 𝑤 𝜓 ) )
3		exdistrv	⊢ ( ∃ 𝑥 ∃ 𝑧 ( ∃ 𝑦 𝜑 ∧ ∃ 𝑤 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 𝜓 ) )
4	2 3	bitri	⊢ ( ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 𝜓 ) )