Theorem 4exbidv

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

	Ref	Expression
Hypothesis	4exbidv.1	|- ( ph -> ( ps <-> ch ) )
Assertion	4exbidv	|- ( ph -> ( E. x E. y E. z E. w ps <-> E. x E. y E. z E. w ch ) )

Proof

Step	Hyp	Ref	Expression
1		4exbidv.1	|- ( ph -> ( ps <-> ch ) )
2	1	2exbidv	|- ( ph -> ( E. z E. w ps <-> E. z E. w ch ) )
3	2	2exbidv	|- ( ph -> ( E. x E. y E. z E. w ps <-> E. x E. y E. z E. w ch ) )