Theorem 2exbidv 1628

Description: Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)

Hypothesis

Ref	Expression
2albidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
2exbidv	|- (ph -> (E.xE.yps <-> E.xE.ych))

Distinct variable groups:   ph,x   ph,y

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

Proof of Theorem 2exbidv

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	exbidv 1626	. 2 |- (ph -> (E.yps <-> E.ych))
3	2	exbidv 1626	1 |- (ph -> (E.xE.yps <-> E.xE.ych))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  3exbidv  1629  4exbidv  1630  cbvex4v  2012  ceqsex3v  2898  ceqsex4v  2899  2reu5  3045  elxpk  4197  cnvkeq  4216  ins2keq  4219  ins3keq  4220  sikeq  4242  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelsikg  4265  sikss1c1c  4268  copsexg  4608  elopab  4697  brsi  4762  elxpi  4801  brswap2  4861  brswap  5510  cbvoprab3  5572  ov6g  5601  brsnsi  5774  dmpprod  5841  ovce  6173  ceex  6175  elce  6176