Theorem 2exbidv 1926

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  3exbidv  1927  4exbidv  1928  cbvex4vw  2044  cbvex4v  2419  ceqsex3v  3483  ceqsex4v  3484  2reu5  3704  opabbidv  5151  unopab  5165  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  euotd  5467  elopabw  5481  elxpi  5653  relop  5805  dfres3  5949  xpdifid  6132  oprabv  7427  cbvoprab3  7458  elrnmpores  7505  ov6g  7531  omxpenlem  9016  dcomex  10369  ltresr  11063  hashle2prv  14440  fsumcom2  15736  fprodcom2  15949  ispos  18280  fsumvma  27176  1pthon2v  30223  dfconngr1  30258  isconngr  30259  isconngr1  30260  1conngr  30264  conngrv2edg  30265  fusgr2wsp2nb  30404  isacycgr  35327  satfv1  35545  sat1el2xp  35561  elfuns  36095  cbvoprab1vw  36419  cbvoprab1davw  36453  cbvoprab3davw  36455  bj-cbvex4vv  37112  itg2addnclem3  37994  brxrn2  38705  dvhopellsm  41563  diblsmopel  41617  2sbc5g  44843  fundcmpsurinj  47869  ichexmpl1  47929  ichnreuop  47932  ichreuopeq  47933  elsprel  47935  prprelb  47976  reuopreuprim  47986  nelsubc3lem  49545  cnelsubclem  50078