Theorem 2exbidv 1922

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

Syntax hints:   → wi 4   ↔ wb 206  ∃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 1908

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

This theorem is referenced by:  3exbidv  1923  4exbidv  1924  cbvex4vw  2039  cbvex4v  2418  ceqsex3v  3537  ceqsex4v  3538  2reu5  3767  opabbidv  5214  unopab  5230  copsexgw  5501  copsexg  5502  euotd  5523  elopabw  5536  elxpi  5711  relop  5864  dfres3  6005  xpdifid  6190  oprabv  7493  cbvoprab3  7524  elrnmpores  7571  ov6g  7597  omxpenlem  9112  dcomex  10485  ltresr  11178  hashle2prv  14514  fsumcom2  15807  fprodcom2  16017  ispos  18372  fsumvma  27272  1pthon2v  30182  dfconngr1  30217  isconngr  30218  isconngr1  30219  1conngr  30223  conngrv2edg  30224  fusgr2wsp2nb  30363  isacycgr  35130  satfv1  35348  sat1el2xp  35364  elfuns  35897  cbvoprab1vw  36220  cbvoprab1davw  36254  cbvoprab3davw  36256  bj-cbvex4vv  36788  itg2addnclem3  37660  brxrn2  38357  dvhopellsm  41100  diblsmopel  41154  2sbc5g  44412  fundcmpsurinj  47334  ichexmpl1  47394  ichnreuop  47397  ichreuopeq  47398  elsprel  47400  prprelb  47441  reuopreuprim  47451