Theorem 2exbidv 1943

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

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

This theorem is referenced by:  3exbidv  1944  4exbidv  1945  cbvex4vw  2061  cbvex4v  2445  ceqsex3v  3505  ceqsex4v  3506  2reu5  3720  opabbidv  5165  unopab  5179  copsexgw  5457  copsexgwOLD  5458  copsexg  5459  euotd  5481  elopabw  5495  elxpi  5667  relop  5820  dfres3  5968  xpdifid  6150  oprabv  7452  cbvoprab3  7483  elrnmpores  7530  ov6g  7556  omxpenlem  9046  dcomex  10401  ltresr  11095  hashle2prv  14488  fsumcom2  15784  fprodcom2  15997  ispos  18329  fsumvma  27254  1pthon2v  30301  dfconngr1  30336  isconngr  30337  isconngr1  30338  1conngr  30342  conngrv2edg  30343  fusgr2wsp2nb  30482  isacycgr  35459  satfv1  35677  sat1el2xp  35693  elfuns  36227  cbvoprab1vw  36561  cbvoprab1davw  36595  cbvoprab3davw  36597  bj-cbvex4vv  37254  itg2addnclem3  38136  brxrn2  38847  dvhopellsm  41705  diblsmopel  41759  2sbc5g  44956  fundcmpsurinj  47979  ichexmpl1  48039  ichnreuop  48042  ichreuopeq  48043  elsprel  48045  prprelb  48086  reuopreuprim  48096  nelsubc3lem  49655  cnelsubclem  50188