Theorem 2exbidv 1957

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  3exbidv  1958  4exbidv  1959  cbvex4vw  2075  cbvex4v  2446  ceqsex3v  3505  ceqsex4v  3506  2reu5  3719  opabbidv  5175  unopab  5189  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  euotd  5494  elopabw  5508  elxpi  5681  relop  5834  dfres3  5981  xpdifid  6164  xpdifcnvepel  6165  oprabv  7477  cbvoprab3  7508  elrnmpores  7555  ov6g  7581  omxpenlem  9080  dcomex  10453  ltresr  11153  hashle2prv  14547  fsumcom2  15864  fprodcom2  16077  ispos  18408  fsumvma  27457  isacycgr  30638  1pthon2v  30641  dfconngr1  30676  isconngr  30677  isconngr1  30678  1conngr  30682  conngrv2edg  30683  fusgr2wsp2nb  30822  satfv1  35950  sat1el2xp  35966  elfuns  36500  cbvoprab1vw  36865  cbvoprab1davw  36899  cbvoprab3davw  36901  bj-cbvex4vv  37556  itg2addnclem3  38430  brxrn2  39140  dvhopellsm  41998  diblsmopel  42052  2sbc5g  45248  fundcmpsurinj  48317  ichexmpl1  48377  ichnreuop  48380  ichreuopeq  48381  elsprel  48383  prprelb  48424  reuopreuprim  48434  nelsubc3lem  50004  cnelsubclem  50537