Theorem 4exbidv 1863

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

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ceqsex8v  2775  copsex4g  4232  opbrop  4690  ovi3  5989  brecop  6603  th3q  6618  dfplpq2  7316  dfmpq2  7317  enq0sym  7394  enq0ref  7395  enq0tr  7396  enq0breq  7398  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708