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  2041  cbvex4v  2419  ceqsex3v  3516  ceqsex4v  3517  2reu5  3741  opabbidv  5185  unopab  5200  copsexgw  5465  copsexg  5466  euotd  5488  elopabw  5501  elxpi  5676  relop  5830  dfres3  5971  xpdifid  6157  oprabv  7467  cbvoprab3  7498  elrnmpores  7545  ov6g  7571  omxpenlem  9087  dcomex  10461  ltresr  11154  hashle2prv  14496  fsumcom2  15790  fprodcom2  16000  ispos  18326  fsumvma  27176  1pthon2v  30134  dfconngr1  30169  isconngr  30170  isconngr1  30171  1conngr  30175  conngrv2edg  30176  fusgr2wsp2nb  30315  isacycgr  35167  satfv1  35385  sat1el2xp  35401  elfuns  35933  cbvoprab1vw  36255  cbvoprab1davw  36289  cbvoprab3davw  36291  bj-cbvex4vv  36823  itg2addnclem3  37697  brxrn2  38393  dvhopellsm  41136  diblsmopel  41190  2sbc5g  44440  fundcmpsurinj  47423  ichexmpl1  47483  ichnreuop  47486  ichreuopeq  47487  elsprel  47489  prprelb  47530  reuopreuprim  47540  nelsubc3lem  49037  cnelsubclem  49480