Theorem 2exbidv 1716

Description: Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)

Hypothesis

Ref	Expression
2albidv.1

Assertion

Ref	Expression
2exbidv

Distinct variable groups:   ,   ,

Proof of Theorem 2exbidv

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3
2	1	exbidv 1714	. 2
3	2	exbidv 1714	1

Syntax hints:  ->wi 4  <->wb 184  E.wex 1612

This theorem is referenced by:  3exbidv  1717  4exbidv  1718  cbvex4v  2034  ceqsex3v  3149  ceqsex4v  3150  2reu5  3308  copsexg  4737  copsexgOLD  4738  euotd  4753  elopab  4760  elxpi  5020  relop  5158  xpdifid  5440  oprabv  6345  cbvoprab3  6373  elrnmpt2res  6416  ov6g  6440  omxpenlem  7638  dcomex  8848  ltresr  9538  fsumcom2  13589  fprodcom2  13788  ispos  15576  fsumvma  23488  dfconngra1  24671  isconngra  24672  isconngra1  24673  1conngra  24675  is2wlkonot  24863  is2spthonot  24864  2wlkonot  24865  2spthonot  24866  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  el2wlkonotot0  24872  2wlkonot3v  24875  2spthonot3v  24876  usg2wotspth  24884  2pthwlkonot  24885  2spotdisj  25061  usg2spot2nb  25065  dfres3  29188  elfuns  29565  itg2addnclem3  30068  2sbc5g  31323  bj-cbvex4vv  34308  dvhopellsm  36844  diblsmopel  36898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-ex 1613