Theorem 2exbidv 1924

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 1921	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1921	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  3exbidv  1925  4exbidv  1926  cbvex4vw  2042  cbvex4v  2413  ceqsex3v  3503  ceqsex4v  3504  2reu5  3729  opabbidv  5173  unopab  5187  copsexgw  5450  copsexg  5451  euotd  5473  elopabw  5486  elxpi  5660  relop  5814  dfres3  5955  xpdifid  6141  oprabv  7449  cbvoprab3  7480  elrnmpores  7527  ov6g  7553  omxpenlem  9042  dcomex  10400  ltresr  11093  hashle2prv  14443  fsumcom2  15740  fprodcom2  15950  ispos  18275  fsumvma  27124  1pthon2v  30082  dfconngr1  30117  isconngr  30118  isconngr1  30119  1conngr  30123  conngrv2edg  30124  fusgr2wsp2nb  30263  isacycgr  35132  satfv1  35350  sat1el2xp  35366  elfuns  35903  cbvoprab1vw  36225  cbvoprab1davw  36259  cbvoprab3davw  36261  bj-cbvex4vv  36793  itg2addnclem3  37667  brxrn2  38357  dvhopellsm  41111  diblsmopel  41165  2sbc5g  44405  fundcmpsurinj  47410  ichexmpl1  47470  ichnreuop  47473  ichreuopeq  47474  elsprel  47476  prprelb  47517  reuopreuprim  47527  nelsubc3lem  49059  cnelsubclem  49592