Theorem 4exbidv

Description: Formula-building rule for four existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995)

	Ref	Expression
Hypothesis	4exbidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	4exbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		4exbidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2	1	2exbidv	⊢ ( 𝜑 → ( ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑧 ∃ 𝑤 𝜒 ) )
3	2	2exbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜒 ) )