Theorem 2exbidv 1921

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

Syntax hints:   → wi 4   ↔ wb 208  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  3exbidv  1922  4exbidv  1923  cbvex4vw  2045  cbvex4v  2433  ceqsex3v  3546  ceqsex4v  3547  2reu5  3749  copsexgw  5374  copsexg  5375  euotd  5396  elopab  5407  elxpi  5572  relop  5716  dfres3  5853  xpdifid  6020  oprabv  7208  cbvoprab3  7239  elrnmpores  7282  ov6g  7306  omxpenlem  8612  dcomex  9863  ltresr  10556  hashle2prv  13830  fsumcom2  15123  fprodcom2  15332  ispos  17551  fsumvma  25783  1pthon2v  27926  dfconngr1  27961  isconngr  27962  isconngr1  27963  1conngr  27967  conngrv2edg  27968  fusgr2wsp2nb  28107  isacycgr  32387  satfv1  32605  sat1el2xp  32621  elfuns  33371  bj-cbvex4vv  34122  itg2addnclem3  34939  brxrn2  35621  dvhopellsm  38247  diblsmopel  38301  2sbc5g  40741  fundcmpsurinj  43562  ichexmpl1  43624  ichnreuop  43627  ichreuopeq  43628  elsprel  43630  prprelb  43671  reuopreuprim  43681