Theorem 4exbidv 1923

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 1921	. 2 |- ( ph -> ( E. z E. w ps <-> E. z E. w ch ) )
3	2	2exbidv 1921	1 |- ( ph -> ( E. x E. y E. z E. w ps <-> E. x E. y E. z E. w ch ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  ceqsex8v  2868  copsex4g  4389  opbrop  4856  ovi3  6229  brecop  6903  th3q  6918  dfplpq2  7727  dfmpq2  7728  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119