Theorem 2exbidv 1927

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

Hypothesis

Ref	Expression
2albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2exbidv	⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2exbidv

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	exbidv 1924	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1924	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  3exbidv  1928  4exbidv  1929  cbvex4vw  2045  cbvex4v  2415  ceqsex3v  3484  ceqsex4v  3485  2reu5  3693  opabbidv  5140  unopab  5156  copsexgw  5404  copsexg  5405  euotd  5427  elopabw  5439  elxpi  5611  relop  5759  dfres3  5896  xpdifid  6071  oprabv  7335  cbvoprab3  7366  elrnmpores  7411  ov6g  7436  omxpenlem  8860  dcomex  10203  ltresr  10896  hashle2prv  14192  fsumcom2  15486  fprodcom2  15694  ispos  18032  fsumvma  26361  1pthon2v  28517  dfconngr1  28552  isconngr  28553  isconngr1  28554  1conngr  28558  conngrv2edg  28559  fusgr2wsp2nb  28698  isacycgr  33107  satfv1  33325  sat1el2xp  33341  elfuns  34217  bj-cbvex4vv  34987  itg2addnclem3  35830  brxrn2  36505  dvhopellsm  39131  diblsmopel  39185  2sbc5g  42034  fundcmpsurinj  44861  ichexmpl1  44921  ichnreuop  44924  ichreuopeq  44925  elsprel  44927  prprelb  44968  reuopreuprim  44978