Theorem 4exbidv 1919

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

Hypothesis

Ref	Expression
4exbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

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

Distinct variable groups:   ph, x   ph, y   ph, z   ph, w

Allowed substitution hints:   ps( x, y, z, w)   ch( x, y, z, w)

Proof of Theorem 4exbidv

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

Syntax hints:   -> wi 4   <-> wb 105   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ceqsex8v  2862  copsex4g  4368  opbrop  4834  ovi3  6199  brecop  6872  th3q  6887  dfplpq2  7685  dfmpq2  7686  enq0sym  7763  enq0ref  7764  enq0tr  7765  enq0breq  7767  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077