Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2rexbidva Unicode version

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
StepHypRef Expression
1 2rexbidva.1 . . . 4
21anassrs 648 . . 3
32rexbidva 2965 . 2
43rexbidva 2965 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator