Theorem 2exbidv 1854

Description: Formula-building rule for two existential quantifiers (deduction rule). (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 1852	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1852	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∃wex 1701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841

This theorem depends on definitions:  df-bi 197  df-ex 1702

This theorem is referenced by:  3exbidv  1855  4exbidv  1856  cbvex4v  2293  ceqsex3v  3237  ceqsex4v  3238  2reu5  3403  copsexg  4921  euotd  4940  elopab  4948  elxpi  5095  relop  5237  xpdifid  5525  oprabv  6657  cbvoprab3  6685  elrnmpt2res  6728  ov6g  6752  omxpenlem  8006  dcomex  9214  ltresr  9906  fsumcom2  14428  fsumcom2OLD  14429  fprodcom2  14634  fprodcom2OLD  14635  ispos  16863  fsumvma  24833  1pthon2v  26873  dfconngr1  26908  isconngr  26909  isconngr1  26910  1conngr  26914  conngrv2edg  26915  fusgr2wsp2nb  27050  dfres3  31349  elfuns  31656  bj-cbvex4vv  32377  itg2addnclem3  33081  dvhopellsm  35872  diblsmopel  35926  2sbc5g  38085  elsprel  41001