Theorem 4exbidv 1842

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 1840	. 2 |- ( ph -> ( E. z E. w ps <-> E. z E. w ch ) )
3	2	2exbidv 1840	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 104   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ceqsex8v  2726  copsex4g  4164  opbrop  4613  ovi3  5900  brecop  6512  th3q  6527  dfplpq2  7155  dfmpq2  7156  enq0sym  7233  enq0ref  7234  enq0tr  7235  enq0breq  7237  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  mulnnnq0  7251  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547