Theorem 4exbidv 1916

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 1914	. 2 |- ( ph -> ( E. z E. w ps <-> E. z E. w ch ) )
3	2	2exbidv 1914	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 1538

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ceqsex8v  2846  copsex4g  4333  opbrop  4798  ovi3  6142  brecop  6772  th3q  6787  dfplpq2  7541  dfmpq2  7542  enq0sym  7619  enq0ref  7620  enq0tr  7621  enq0breq  7623  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  mulnnnq0  7637  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933