Theorem reximdva 3017

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
reximdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
reximdva	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 450	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 3015	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  reximddv  3018  reximdvva  3019  reximddv2  3020  wereu2  5111  dffo4  6375  nnaordex  7718  frfi  8205  fisupg  8208  marypha1  8340  fiinfg  8405  wemapsolem  8455  unwdomg  8489  rankr1ai  8661  cofsmo  9091  cfcoflem  9094  inar1  9597  nqerf  9752  prlem936  9869  fimaxre  10968  arch  11289  bndndx  11291  suprfinzcl  11492  zmin  11784  qbtwnxr  12031  qsqueeze  12032  qextltlem  12033  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrunb1  12149  ssnn0fi  12784  fsuppmapnn0fiub0  12793  fsuppmapnn0fz  12796  expnlbnd2  12995  r19.29uz  14090  cau3lem  14094  rlim2lt  14228  rlimclim  14277  2clim  14303  o1co  14317  climcn1  14322  climcn2  14323  rlimo1  14347  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  lo1le  14382  climsup  14400  climcau  14401  caucvgrlem2  14405  iseralt  14415  cvgcmp  14548  cvgcmpce  14550  supcvg  14588  rpnnen2lem12  14954  bezoutlem1  15256  divgcdcoprmex  15380  exprmfct  15416  prmdvdsfz  15417  pclem  15543  pc2dvds  15583  pcprmpw  15587  dvdsprmpweqle  15590  unbenlem  15612  infpnlem2  15615  infpn2  15617  prmunb  15618  vdwlem2  15686  ramub1lem2  15731  prmdvdsprmop  15747  prmgaplem7  15761  ipodrsima  17165  grpinveu  17456  dfgrp3lem  17513  psgneu  17926  odbezout  17975  sylow2blem3  18037  nn0gsumfz  18380  ringadd2  18575  irredrmul  18707  lbsextlem2  19159  mptcoe1fsupp  19585  znunit  19912  scmate  20316  scmatscm  20319  scmatfo  20336  mat1scmat  20345  pmatcoe1fsupp  20506  pmatcollpwfi  20587  pmatcollpw3fi  20590  mptcoe1matfsupp  20607  pm2mp  20630  chmaidscmat  20653  cpmadumatpoly  20688  chcoeffeq  20691  cayhamlem3  20692  cayhamlem4  20693  neiptopnei  20936  neitr  20984  cnpnei  21068  haust1  21156  isnrm3  21163  isreg2  21181  tgcmp  21204  hauscmplem  21209  hauscmp  21210  bwth  21213  1stcfb  21248  1stcelcls  21264  lly1stc  21299  txcmplem1  21444  txlm  21451  xkococnlem  21462  filuni  21689  filufint  21724  ufilen  21734  fclscf  21829  cnextcn  21871  ustex2sym  22020  ustex3sym  22021  utopreg  22056  isucn2  22083  ucnima  22085  ucncn  22089  neipcfilu  22100  metequiv2  22315  metrest  22329  xrsmopn  22615  mulc1cncf  22708  cncfco  22710  bndth  22757  lmmcvg  23059  cfil3i  23067  iscau4  23077  cmetcaulem  23086  iscmet3lem1  23089  caussi  23095  equivcfil  23097  equivcau  23098  caubl  23106  minveclem3b  23199  ovolgelb  23248  ovollb2lem  23256  ovolctb  23258  ovolicc2lem4  23288  ioombl1lem4  23329  dyadmax  23366  volsup2  23373  itg2monolem1  23517  c1liplem1  23759  c1lip1  23760  dvivthlem1  23771  lhop1  23777  ftc1a  23800  ftc1lem6  23804  ply1divex  23896  elply2  23952  dgrlem  23985  aacjcl  24082  aalioulem2  24088  aalioulem3  24089  aalioulem4  24090  ulmcaulem  24148  ulmcau  24149  ulmss  24151  mtest  24158  itgulm  24162  reeff1o  24201  efif1olem4  24291  rlimcnp  24692  xrlimcnp  24695  lgamucov  24764  ftalem3  24801  fta  24806  muval1  24859  dvdssqf  24864  mumullem1  24905  lgsqrmod  25077  lgsqrmodndvds  25078  pntlem3  25298  ostth  25328  tgtrisegint  25394  tgbtwndiff  25401  tgcgrxfr  25413  lnext  25462  legov2  25481  legtrd  25484  hlcgrex  25511  colperpexlem3  25624  colperpex  25625  hlpasch  25648  hpgerlem  25657  hpgtr  25660  dfcgra2  25721  acopy  25724  inagswap  25730  inaghl  25731  cgrg3col4  25734  axpasch  25821  wwlksnredwwlkn0  26791  midwwlks2s3  26860  2pthfrgrrn2  27147  frgrwopreg1  27182  frgrwopreg2  27183  grpoidinvlem3  27360  grpoideu  27363  grpoinveu  27373  ubthlem1  27726  minvecolem5  27737  htthlem  27774  chscllem2  28497  nmopun  28873  lnconi  28892  rnbra  28966  sumdmdii  29274  cdj3lem2b  29296  foresf1o  29343  acunirnmpt  29459  xrofsup  29533  fprodex01  29571  isarchi3  29741  isarchiofld  29817  lmxrge0  29998  lmdvg  29999  esumlub  30122  esumfsup  30132  esumcvg  30148  ftc2re  30676  cvmliftmolem2  31264  cvmlift2lem12  31296  frmin  31739  wzel  31771  wzelOLD  31772  wsuclem  31773  wsuclemOLD  31774  nosupno  31849  nosupbnd1lem4  31857  conway  31910  btwndiff  32134  trisegint  32135  cgrxfr  32162  lineext  32183  segcon2  32212  brsegle2  32216  seglecgr12im  32217  segletr  32221  broutsideof3  32233  opnrebl2  32316  nn0prpw  32318  fin2so  33396  poimirlem27  33436  poimirlem30  33439  poimirlem31  33440  poimir  33442  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  ftc1cnnc  33484  ftc1anclem5  33489  sdclem1  33539  geomcau  33555  equivtotbnd  33577  bndss  33585  ismtybndlem  33605  heibor1lem  33608  rrncmslem  33631  rngo2  33706  prtlem15  34160  lsateln0  34282  lsat0cv  34320  eqlkr3  34388  lkrshp  34392  lshpset2N  34406  hlhgt2  34675  hlrelat2  34689  atle  34722  athgt  34742  2dim  34756  1cvratex  34759  ps-2  34764  dalem20  34979  lhpexle1lem  35293  lhpexle1  35294  lhpexle2lem  35295  lhpmcvr5N  35313  lhpmcvr6N  35314  cdleme25a  35641  cdleme29ex  35662  cdlemfnid  35852  cdlemg33b0  35989  cdlemg33a  35994  cdlemg35  36001  cdleml3N  36266  dihlsscpre  36523  dih1dimb2  36530  dihatexv  36627  dvh3dim2  36737  dochkr1  36767  dochkr1OLDN  36768  lcfl8  36791  lcfl8b  36793  lcfrlem5  36835  lcfrlem6  36836  mapdrvallem2  36934  mapdh9a  37079  mapdh9aOLDN  37080  hdmaprnlem3eN  37150  hdmaprnlem16N  37154  fphpdo  37381  rencldnfilem  37384  irrapxlem2  37387  cvgdvgrat  38512  expgrowth  38534  projf1o  39386  rnmptlb  39453  rnmptbddlem  39455  rnmptbd2lem  39463  ssfiunibd  39523  supxrgere  39549  supxrgelem  39553  suplesup  39555  infrpge  39567  infleinf  39588  supxrunb3  39623  unb2ltle  39642  uzub  39658  qinioo  39762  qelioo  39773  climinf  39838  mullimc  39848  islptre  39851  limccog  39852  mullimcf  39855  limcrecl  39861  sumnnodd  39862  neglimc  39879  0ellimcdiv  39881  limclner  39883  allbutfifvre  39907  climleltrp  39908  fnlimabslt  39911  climinf2lem  39938  limsuppnflem  39942  limsupvaluz2  39970  supcnvlimsup  39972  limsupgtlem  40009  liminflelimsupuz  40017  liminflimsupclim  40039  cncfioobd  40110  stoweidlem7  40224  stoweidlem27  40244  stoweidlem39  40256  stoweidlem48  40265  stoweidlem49  40266  stoweidlem60  40277  stoweidlem61  40278  stoweid  40280  dirkercncflem2  40321  fourierdlem20  40344  fourierdlem39  40363  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem64  40387  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  qndenserrnopnlem  40517  sge0ltfirp  40617  sge0gerpmpt  40619  sge0ltfirpmpt2  40643  sge0isum  40644  sge0pnffigtmpt  40657  sge0pnffsumgt  40659  sge0gtfsumgt  40660  sge0uzfsumgt  40661  nnfoctbdjlem  40672  meaiuninclem  40697  omeiunltfirp  40733  carageniuncllem2  40736  hoicvr  40762  volicorescl  40767  hoidmv1le  40808  hoidmvlelem3  40811  hoiqssbllem3  40838  hspmbllem2  40841  iunhoiioolem  40889  vonioo  40896  vonicc  40899  smfaddlem1  40971  smflimlem2  40980  smflimlem3  40981  smfmullem4  41001  2pwp1prmfmtno  41504  proththd  41531  sbgoldbwt  41665  sbgoldbst  41666  sbgoldbalt  41669  bgoldbtbndlem4  41696  bgoldbtbnd  41697  zrninitoringc  42071  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177  islindeps2  42272  isldepslvec2  42274