Theorem 2exbidv 1947

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  3exbidv  1948  4exbidv  1949  cbvex4vw  2065  cbvex4v  2449  ceqsex3v  3509  ceqsex4v  3510  2reu5  3724  opabbidv  5171  unopab  5185  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  euotd  5487  elopabw  5501  elxpi  5674  relop  5827  dfres3  5974  xpdifid  6157  xpdifcnvepel  6158  oprabv  7460  cbvoprab3  7491  elrnmpores  7538  ov6g  7564  omxpenlem  9054  dcomex  10419  ltresr  11113  hashle2prv  14505  fsumcom2  15815  fprodcom2  16028  ispos  18360  fsumvma  27335  1pthon2v  30413  dfconngr1  30448  isconngr  30449  isconngr1  30450  1conngr  30454  conngrv2edg  30455  fusgr2wsp2nb  30594  isacycgr  35508  satfv1  35726  sat1el2xp  35742  elfuns  36276  cbvoprab1vw  36610  cbvoprab1davw  36644  cbvoprab3davw  36646  bj-cbvex4vv  37302  itg2addnclem3  38184  brxrn2  38895  dvhopellsm  41753  diblsmopel  41807  2sbc5g  44990  fundcmpsurinj  48013  ichexmpl1  48073  ichnreuop  48076  ichreuopeq  48077  elsprel  48079  prprelb  48120  reuopreuprim  48130  nelsubc3lem  49699  cnelsubclem  50232