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  3494  ceqsex4v  3495  2reu5  3720  opabbidv  5161  unopab  5175  copsexgw  5437  copsexg  5438  euotd  5460  elopabw  5473  elxpi  5645  relop  5797  dfres3  5939  xpdifid  6121  oprabv  7413  cbvoprab3  7444  elrnmpores  7491  ov6g  7517  omxpenlem  9002  dcomex  10360  ltresr  11053  hashle2prv  14403  fsumcom2  15699  fprodcom2  15909  ispos  18238  fsumvma  27140  1pthon2v  30115  dfconngr1  30150  isconngr  30151  isconngr1  30152  1conngr  30156  conngrv2edg  30157  fusgr2wsp2nb  30296  isacycgr  35117  satfv1  35335  sat1el2xp  35351  elfuns  35888  cbvoprab1vw  36210  cbvoprab1davw  36244  cbvoprab3davw  36246  bj-cbvex4vv  36778  itg2addnclem3  37652  brxrn2  38342  dvhopellsm  41096  diblsmopel  41150  2sbc5g  44389  fundcmpsurinj  47394  ichexmpl1  47454  ichnreuop  47457  ichreuopeq  47458  elsprel  47460  prprelb  47501  reuopreuprim  47511  nelsubc3lem  49056  cnelsubclem  49589