Theorem 2rexbidva 2974

Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)

Hypothesis

Ref	Expression
2rexbidva.1

Assertion

Ref	Expression
2rexbidva

Distinct variable groups:   ,,   ,

Proof of Theorem 2rexbidva

Step	Hyp	Ref	Expression
1		2rexbidva.1	. . . 4
2	1	anassrs 648	. . 3
3	2	rexbidva 2965	. 2
4	3	rexbidva 2965	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  E.wrex 2808

This theorem is referenced by:  bezoutlem2  14177  bezoutlem4  14179  vdwmc2  14497  lsmcom2  16675  lsmass  16688  lsmcomx  16862  lsmspsn  17730  hausdiag  20146  imasf1oxms  20992  istrkg2ld  23858  axeuclid  24266  el2wlksot  24880  el2pthsot  24881  usg2spot2nb  25065  shscom  26237  2reu4a  32194  pgrpgt2nabl  32959  3dim0  35181  islpln5  35259  islvol5  35303  isline2  35498  isline3  35500  paddcom  35537  cdlemg2cex  36317

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-an 371  df-ex 1613  df-rex 2813